Formal Methods are techniques used to prevent errors on the development of Software Systems. As the process of developing Software from Formal methods is laborious and error-prone, Formal Code Generators are used. The use of these tools reduces error odds on the implementation of Software Systems from Formal Specifications. As there can be errors also on the process of generation of the Software from the input Specification, an interesting effort is to prove that the generated code correctly implements the input specification. This Qualifying Doctorate Proposal aims at elaborating a coverage and code-model-checking based strategy to validate JCircus, a translator from concrete Circus’ specifications to Java code. This validation strategy encompasses the implementation of a Labelled Transition System Generator (LPTSGen) for Circus (based on a Structural Operational Semantics for Circus ) and its conversion to JPF (Java Pathfinder), a Java model checker. The goal is to check if the specification is refined by the generated code by JCircus. In order to achieve this goal, the JPF model must conduct the generated code by JCircus. 

 

This Doctorate Proposal also shows partial results on the proof of soundness of the rules of the Structural Operational Semantics with respect to the Unifying Theories of Programming (UTP). The role of the proof of soundness is to strenghten the validation.