ASLAN(ID:7843/)
Specificatino language
Related languages
| ASLAN |
=> |
ASTRAL | |
Influence |
| ASLAN |
=> |
RT-ASLAN | |
Evolution of |
| ASLAN |
=> |
TRIO | |
Evolution of |
References:
Auernheimer, B. and D. Stearns. Using the ASLAN formal specification language in undergraduate software engineering courses. Computer Science Education, vol. 2 (2-3). view details
Brent Auernheimer and Richard A. Kemmerer "ASLAN User?s Manual" Reliable Software Group Tech Report TRCS84-10 Department of Computer Science UCSB 1992 view details
Abstract: This document serves as a guide to the ASLAN specification language and use of the ASLAN language processor. Section 1 introduces the strategies underlying the ASLAN approach to system specification. A small, syntactically correct specification is presented to serve as motivation for the detailed exposition to follow.
The second and largest section of this document describes the syntax and semantics of the ASLAN language. Following sections describe the use of the ASLAN language processor and further explain the ASLAN approach towards correctness and consistency conjectures. A non-trivial, syntactically correct specification example and associated correctness conjectures are presented in the final section.
Extract: An Overview of Correctness Conjectures
An Overview of Correctness Conjectures
How does ASLAN guarantee that a specification is "correct"? A reasonable goal would be to show that the system defined by the state variables and transitions always satisfies some critical requirements. These critical requirements must be met in every state that the system may reach. In ASLAN terminology these requirements are state invariants. To prove that a specification satisfies some invariant assertion, ASLAN generates proof obligations needed to construct an inductive proof of the correctness of the specification with respect to the invariant assertion. These proof obligations are known as correctness conjectures. It is the user's responsibility to establish the validity of the correctness conjectures, possibly with the aid of a theorem prover. As the basis of the induction it must be shown that the system starts only in states that satisfy the state invariant.
Douglas, Jeffrey G. "Aslantest User''s Manual", University of California at Santa Barbara, Santa Barbara, CA, 1994 view details
Douglas, Jeffrey G. "Xaslantest User Manual", University of California at Santa Barbara, Santa Barbara, CA, 1994
view details
Jeffrey Douglas, Richard A. Kemmerer: Aslantest: A Symbolic Execution Tool for Testing Aslan Formal Specifications. ISSTA 1994: 15-27 view details
Abstract: 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.
DOI
|