Aslantest: a symbolic execution tool for testing Aslan formal specifications

摘要

This paper introduces Aslantest, a symbolic execution tool for the formal specification language Aslan. Aslan is a state-based specification language built on first-order predicate calculus with equality. Aslantest animates Aslan specifications and enables users to interactively run specific test cases or symbolically execute the specification. Testing the formal specifications early in the software life cycle allows one to assure a reliable system that also provides the desired functionality.