Generation of Java programs properties from test purposes
Simone Hanazumi, Ana C. V. de Melo · 2013
Software formal verification is a technique used to ensure that computational systems have high-quality and work properly. From the system specification described in a formal language, we define properties that must be satisfied during system execution to guarantee the software quality. Then, these properties should be implemented in a verifier, tool responsible for running the verification and for notifying which properties were satisfied or not. When the verification process finishes, the verifier will indicate to software developers the possible location of each code fault in the system. The disadvantages of using formal verification are the high cost to apply this technique in real systems, and the necessity of having people with experience in formal languages and formal methods. In addition, the implementation of properties related to a particular system in a verifier is a complex task.