Loading...
Please wait, while we are loading the content...
Similar Documents
Requirements validation by lifting retrenchments in b.
| Content Provider | CiteSeerX |
|---|---|
| Author | Poppleton, Michael Banach, Richard |
| Abstract | Simple retrenchment is briefly reviewed in the B specification language of J.-R. Abrial [1] as a liberalization of classical refinement, for the formal description of application developments too demanding for refinement. The looser relationships allowed by retrenchment between adjacent models in the development process may capture some of the requirements information of the development. This can make requirements validation more difficult to understand since the locus of requirements should be the models, and not their interrelationships, as far as possible. Hence the universal construction of [6], originally proposed for simple transition systems, is reformulated in B, in order to "lift" a given retrenchment conceptually, thus retracting such requirements information back to the level of abstraction of the abstract, ideal model. Examples demonstrate the cognitive value of retracting requirements to the abstract level, articulated in a well-understood formal language. This is also seen to yield a more understandable way of comparing alternative retrenchment designs. Some new B syntax in the pre- and postcondition style is presented to facilitate expression of the lifted requirements. |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Requirement Validation Requirement Information Universal Construction Simple Transition System Alternative Retrenchment Design Lifted Requirement Simple Retrenchment Understandable Way New Syntax Abstract Level Ideal Model Cognitive Value Formal Description Classical Refinement Adjacent Model Postcondition Style Development Process Specification Language Application Development Well-understood Formal Language |
| Content Type | Text |
