NDLI: XFM: An incremental methodology for developing formal models

Content Provider	ACM Digital Library
Author	Shukla, Sandeep K. Berner, David Mathaikutty, Deepak A. Suhaib, M.
Copyright Year	2005
Abstract	We present an agile formal methodology named eXtreme Formal Modeling (XFM), based on Extreme Programming (XP) concepts to construct abstract models from natural language specifications of complex systems. In particular, we focus on Prescriptive Formal Models (PFMs) that capture the specification of the system under design in a mathematically precise manner. Such models can be used as golden reference models for formal verification, test generation, coverage monitor generation, etc. This methodology for incrementally building PFMs works by adding user stories expressed as LTL formulae gleaned from the natural language specifications, one by one, into the model. XFM builds the models, retaining correctness with respect to incrementally added properties by regressively model-checking all the LTL properties captured theretofore in the model. We illustrate XFM with a graded set of examples consisting of a traffic light controller and a DLX pipeline. To make the regressive model-checking steps feasible with current model-checking tools, we need to control the model size increments at each subsequent step in the process. We therefore analyze the effects of ordering the LTL properties in XFM on the statespace growth rate of the model. We compare three different property-ordering methodologies: ad hoc ordering, property-based ordering, and predicate-based ordering. We experiment on the models of the ISA bus monitor and the arbitration phase of the Pentium Pro bus. We experimentally show and mathematically reason that the predicate-based ordering is the best among these orderings. Finally, we present a GUI-based toolbox that we implemented to build PFMs using XFM.
Starting Page	589
Ending Page	609
Page Count	21
File Format	PDF
ISSN	10844309
e-ISSN	15577309
DOI	10.1145/1109118.1109120
Volume Number	10
Issue Number	4
Journal	ACM Transactions on Design Automation of Electronic Systems (TODAES)
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2005-10-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Extreme formal modeling SMV SPIN Extreme programming Formal specification Formal verification Prescriptive formal models Property ordering Property refactoring
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Computer Science Applications Electrical and Electronic Engineering

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

D.: XFM: An Incremental Methodology for Developing Formal Models (2005)

Xfm: an incremental methodology for developing formal models (2004).

XFM: An Incremental Methodology for Developing Formal Models (2005)

XFM: Extreme Formal Method for Capturing Formal Specification into Abstract Models (2003)

An industrially effective environment for formal hardware verification

Extreme Formal Modeling (XFM) for Hardware Models

On attaining reliable software for a secure operating system

Specification and verification of pipelining in the ARM2 RISC microprocessor

ATM switch design by high-level modeling, formal verification and high-level synthesi

XFM: An incremental methodology for developing formal models

Similar Documents

D.: XFM: An Incremental Methodology for Developing Formal Models (2005)

Xfm: an incremental methodology for developing formal models (2004).

XFM: An Incremental Methodology for Developing Formal Models (2005)

XFM: Extreme Formal Method for Capturing Formal Specification into Abstract Models (2003)

An industrially effective environment for formal hardware verification

Extreme Formal Modeling (XFM) for Hardware Models

On attaining reliable software for a secure operating system

Specification and verification of pipelining in the ARM2 RISC microprocessor

ATM switch design by high-level modeling, formal verification and high-level synthesi

XFM: An incremental methodology for developing formal models