NDLI: Requirements validation by lifting retrenchments in B

Content Provider	IEEE Xplore Digital Library
Author	Poppleton, M. Banach, R.
Copyright Year	2004
Description	Author affiliation: Sch. of Electron. & Comput. Sci., Southampton Univ., UK (Poppleton, M.)
Abstract	Simple retrenchment is briefly reviewed in the B specification language of J.-R. Abrial (1996) 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 by Banach (2000), 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.
Sponsorship	IEEE Comput. Soc. Tech. Committee on Complexity in Computing
Starting Page	87
Ending Page	96
File Size	351991
Page Count	10
File Format	PDF
ISBN	0769521096
ISSN	10504729
DOI	10.1109/ICECCS.2004.1310907
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2004-04-16
Publisher Place	Italy
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Concrete Computer science Information retrieval Specification languages Application software Formal languages Mathematical model Mathematics Robustness Control engineering
Content Type	Text
Resource Type	Article
Subject	Artificial Intelligence Control and Systems Engineering Electrical and Electronic Engineering Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Model-based formal specification directed testing of abstract data types

software engineering and artificial intelligence

Instrumented logical sensor systems-practice

Issues surrounding specification languages for software automation

A formal model for output multimodal HCI : An Event-B formalization

A conceptual framework for state-based and event-based formal behavioural specification languages

Requirements validation by lifting retrenchments in b.

Standards and techniques for object-oriented formal specification

Informal and formal requirements specification languages: bridging the gap

Requirements validation by lifting retrenchments in B

Similar Documents

Model-based formal specification directed testing of abstract data types

software engineering and artificial intelligence

Instrumented logical sensor systems-practice

Issues surrounding specification languages for software automation

A formal model for output multimodal HCI : An Event-B formalization

A conceptual framework for state-based and event-based formal behavioural specification languages

Requirements validation by lifting retrenchments in b.

Standards and techniques for object-oriented formal specification

Informal and formal requirements specification languages: bridging the gap

Requirements validation by lifting retrenchments in B