NDLI: Automatic generation of state invariants from requirements specifications

Content Provider	ACM Digital Library
Author	Jeffords, Ralph Heitmeyer, Constance
Abstract	Automatic generation of state invariants, properties that hold in every reachable state of a state machine model, can be valuable in software development. Not only can such invariants be presented to system users for validation, in addition, they can be used as auxiliary assertions in proving other invariants. This paper describes an algorithm for the automatic generation of state invariants that, in contrast to most other such algorithms, which operate on programs, derives invariants from requirements specifications. Generating invariants from requirements specifications rather than programs has two advantages: 1) because requirements specifications, unlike programs, are at a high level of abstraction, generation of and analysis using such invariants is easier, and 2) using invariants to detect errors during the requirements phase is considerably more cost-effective than using invariants later in software development. To illustrate the algorithm, we use it to generate state invariants from requirements specifications of an automobile cruise control system and a simple control system for a nuclear plant. The invariants are derived from specifications expressed in the SCR (Software Cost Reduction) tabular notation.
Starting Page	56
Ending Page	69
Page Count	14
File Format	PDF
ISSN	01635948
DOI	10.1145/291252.288218
Journal	ACM SIGSOFT Software Engineering Notes (SOEN)
Volume Number	23
Issue Number	6
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1979-04-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Validation Specification Verification Formal methods Software tools Invariants Requirements
Content Type	Text
Resource Type	Article

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

Automatic generation of state invariants from requirements specifications

A strategy for efficiently verifying requirements

Automatic generation of formal specification from requirements definition

Verification and Validation for Trustworthy Software Systems

Mechanical verification and automatic implementation of communication protocols

A strategy for efficiently verifying requirements

Tools for formal specification, verification, and validation of requirements

Formal Specification and Verification of Industrial Control Logic Components

Testing Formal Specifications to Detect Design Errors

Automatic generation of state invariants from requirements specifications

Similar Documents

Automatic generation of state invariants from requirements specifications

A strategy for efficiently verifying requirements

Automatic generation of formal specification from requirements definition

Verification and Validation for Trustworthy Software Systems

Mechanical verification and automatic implementation of communication protocols

A strategy for efficiently verifying requirements

Tools for formal specification, verification, and validation of requirements

Formal Specification and Verification of Industrial Control Logic Components

Testing Formal Specifications to Detect Design Errors

Automatic generation of state invariants from requirements specifications