Elucidation and specification of software properties through patterns and composite propositions to support formal verification techniques

Software practitioners have not widely adopted formal verification techniques in spite of the ability of these techniques to improve program dependability and detect errors not captured by other verification approaches. The main reasons are the high level of mathematical training required to specify properties, the lack of tool support for formal specification, and the difficulty of reading and understanding specifications, making them challenging to validate. The dissertation addresses these problems through the Property Specification (Prospec) framework. Prospec makes use of decision trees, timeline diagrams, graphical representation of a computation, and Petri nets to elucidate program behavior associated with patterns from the Specification Pattern System (SPS). Prospec is based on the revised SPS semantics that resulted after a detailed analysis of SPS\u27s limitations. The presented research defined the Composite Proposition (CP) taxonomy, a characterization of sequential and concurrent behavioral structures. Prospec uses CP with SPS to support a set of property patterns that is more comprehensive than other approaches. The visual abstractions used by Prospec highlight subtle details in the structure of the behavior that differentiate scopes, patterns, and CP classes. The research defined and proved the correctness of the mappings that support the automatic generation of formal specifications in Future Interval Logic (FIL) and the Meta Event Definition Language (MEDL). The FIL and MEDL specifications can be used by theorem provers and monitoring systems, respectively, to verify properties of programs. The result of a formal experiment provides empirical evidence of the effectiveness of Prospec. The research is significant because it supports the generation of correct formal specifications that can be used by a variety of formal verification techniques; it provides an approach for clarifying and understanding properties, in particular those related to sequential and concurrent properties that are characteristic of reactive systems; and it resulted in a tool that can be used to learn formal specification languages