Automated Analysis Tools

Penelope

Penelope [Gua90] is a prototype system for the interactive development and verification of programs written in a rich subset of sequential Ada. Because it generates verification conditions incrementally, Penelope can be used to develop a program and its correctness proof in concert. If an already-verified program is modified, one can attempt to prove the modified version by replaying and modifying the original sequence of proof steps. Verification conditions are generated by predicate transformers whose logical soundness can be proven by establishing a precise formal connection between predicate transformation and denotational definitions in the style of continuation semantics. Penelope’s specification language, Larch/Ada, belongs to the family of Larch interface languages.

Larch/VHDL

Larch/VHDL [Bic96, Bic99, Bic00] is an interactive system for specifying and verifying hardware designs written in VHDL. It supports compositional reasoning, automates many routine verification tasks, and operates directly on the engineer’s VHDL code (not a translation into some other formalism). [Bic00] describes the use of Larch/VHDL to verify a 10,000 line VHDL design created by Motorola engineers to implement the instruction set of the ARM7 microprocessor (from Advance RISC Machines). The verification effort included creation of a complete formal specification for the programmer’s model of the ARM7.

Tablewise

Decision tables are widely used for specifying finite functions, such as finite state transitions. Tablewise [Hoo95] tests decision tables for completeness (an output is specified for every possible input) and consistency (no more than one output is specified for any input). Tablewise also supports a novel form of structural analysis that localizes flaws that cause inconsistency or incompleteness. It can generate Ada code that implements the function defined by a decision table and can generate English-language documentation describing that function.

References

[Gua90] D. Guaspari, C. Marceau, and W. Polak. Formal verification of Ada programs. IEEE Transactions on Software Engineering, 16(9):1058-1075, September 1990. http://doi.ieeecomputersociety.org/10.1109/32.58790

[Bic96] M. Bickford and D. Jamsek. Formal specification and verification of VHDL. In Formal Methods in Computer-Aided Design (FM-CAD), (Mandayam Srivas and Albert Camilleri, editors) LNCS 1166. Springer-Verlag, 1996. http://www.springerlink.com/content/mxtm878753756w65/

[Bic99] M. Bickford and D. Naydich. Verification of LRP150. Odyssey Research Associates Technical Report, 1999-0010.

[Bic00] M. Bickford. Verifying a pipelined microprocessor. In Proceedings of the 19th Digital Avionics Systems Conferences (DASC), vol. 1, pages 1A5/1-1A5/8, 2000. http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=886876

[Hoo95] D.N. Hoover and Z. Chen, Z. Tablewise, a decision table tool. In Proceedings of the 10th Annual Conference on Computer Assurance (COMPASS '95) (Gaithersburg, MD., June). IEEE, New York, pp. 97-108. http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=521890