Title :
A Formal Approach for the Iterative Design of Behavioural Models
Author_Institution :
McMaster Centre for Software Certification, McMaster Univ., Hamilton, ON, Canada
Abstract :
In the process of specifying update operations of an information system, it is critical to ensure that the resulting design is consistent with the developers´ understanding about the requirements, before it is adapted to a chosen platform of implementation. We present a formal approach to testing behavioral specifications that characterise the intended effects on the state as two-state, first-order predicates. By supplying use-case scenarios that are of interest, the developers are able to examine the test results, decide if the model under test is consistent, and revise the source specifications if necessary. To facilitate an iterative process of this, in this paper we develop a list of equivalence and refinement (rewriting) laws of predicates that are targeted at information system states. Our development is built upon the formal semantics and logical properties of a formal language of substitutions that serves as an abstract implementation language for these predicates.
Keywords :
formal specification; behavioral specification; behavioural models; equivalence; formal language; formal semantics; information system states; iterative design; logical property; model under test; source specification; update operation; use case scenario; Abstracts; Adaptation models; Information systems; Resource management; Semantics; Standards; Testing; Information Systems; Iterative Design; Model-Based Testing; Weakest Precondition Semantics;
Conference_Titel :
Software Engineering Conference (APSEC), 2012 19th Asia-Pacific
Conference_Location :
Hong Kong
Print_ISBN :
978-1-4673-4930-7
DOI :
10.1109/APSEC.2012.125