1997 Workshop on Engineering of Computer-Based Systems (ECBS '97)
Representing abstract architectures with axiomatic specifications and activation conditions
Monterey, CA
March 24-March 28
ISBN: 0-8186-7889-5
P. Baraona, Dept. of Electr. & Comput. Eng. & Comput. Sci., Cincinnati Univ., OH, USA
P. Alexander, Dept. of Electr. & Comput. Eng. & Comput. Sci., Cincinnati Univ., OH, USA
Evaluating architectural design decisions early in the design process is critical for cost effective design. Formal analysis can provide such evaluation if architectures are defined in a formal way. This paper describes how VSPEC can be used to formally define an architecture during requirements specification. VSPEC is a Larch interface language for VHDL that annotates VHDL entities using the axiomatic style provided by Larch interface languages. Using VHDL's structural definition support, entities described in this manner are connected to form architectural descriptions. Activation conditions over component inputs define when that component must perform its transform. In this paper, we formally define a VSPEC component's state and how component states interact in an architecture. A rudimentary formal semantics for component activation is presented and used to define two potential satisfaction criterion.
Index Terms:
formal specification; abstract architectures representation; axiomatic specifications; activation conditions; formal analysis; VSPEC; Larch interface language; VHDL; axiomatic style; formal semantics
Citation:
P. Baraona, P. Alexander, "Representing abstract architectures with axiomatic specifications and activation conditions," ecbs, pp.161, 1997 Workshop on Engineering of Computer-Based Systems (ECBS '97), 1997