Patent ID: 7281237

Claim:
A method for software development comprising: creating a formal specification of a software program; verifying said formal specification; creating an executable form of said formal specification; creating an implementation of said software program, said implementation including program source code and at least one annotation from said formal specification wherein said implementation of said software program is different from said formal specification; creating an executable program based on said implementation of said software program, said executable program including at least one reference to said executable form of said formal specification, wherein said creating an executable program includes: receiving said implementation including program source code and at least one annotation from said formal specification by an annotation compiler including an extractor/syntax checker; a compiler; a linker; and a cross-linker; extracting, by said extractor/syntax checker, said at least one annotation from said implementation; presenting, by said extractor/syntax checker, said at least one annotation to said cross-linker; compiling, by said compiler, said program source code to generate compiled code including compiled source code modules; presenting, by said compiler, said compiled code to said linker; resolving, by said linker, references between said compiled source code modules to generate implementation executable code; presenting, by said linker, said implementation executable code to said cross linker; and linking, by said cross linker, said implementation executable code and said at least one annotation to create said executable program including said implementation executable code linked to said executable form of said formal specification; and executing said executable program to perform real-time verification of said program implementation with said formal specification.