XFM: An Incremental Methodology for Developing Formal Models

Show simple item record

dc.contributor.advisor Shukla, Sandeep K. en_US
dc.contributor.advisor Ravindran, Binoy en_US
dc.contributor.advisor Ha, Dong S. en_US
dc.contributor.author Suhaib, Syed Mohammed en_US
dc.date.accessioned 2011-08-06T16:01:28Z
dc.date.available 2011-08-06T16:01:28Z
dc.date.issued 2004-05-07 en_US
dc.identifier.other etd-05102004-195753 en_US
dc.identifier.uri http://hdl.handle.net/10919/9905
dc.description.abstract We present a methodology of an agile formal method named eXtreme Formal Modeling (XFM) recently developed by us, based on Extreme Programming concepts to construct abstract models from a natural language specification of a complex system. 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, etc. This methodology for incrementally building PFMs work 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 including a traffic light controller, a DLX pipeline and a Smart Building control system. To make the regressive model checking steps feasible with current model checking tools, we need to keep the model size increments under control. We therefore analyze the effects of ordering LTL properties in XFM. We compare three different property-ordering methodologies: 'arbitrary 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 predicate based ordering is the best among these orderings. Finally, we present a GUI based toolbox for users to build PFMs using XFM. en_US
dc.format.medium ETD en_US
dc.publisher Virginia Tech en_US
dc.relation.haspart suhaib_thesis.pdf en_US
dc.rights The authors of the theses and dissertations are the copyright owners. Virginia Tech's Digital Library and Archives has their permission to store and provide access to these works. en_US
dc.source.uri http://scholar.lib.vt.edu/theses/available/etd-05102004-195753 en_US
dc.subject Formal Verification en_US
dc.subject SPIN en_US
dc.subject SMV en_US
dc.subject Embedded Systems en_US
dc.subject Property Refactoring en_US
dc.subject Prescriptive Formal Models en_US
dc.subject Extreme Modeling en_US
dc.subject Property Ordering en_US
dc.subject Extreme Programming en_US
dc.title XFM: An Incremental Methodology for Developing Formal Models en_US
dc.type Thesis en_US
dc.contributor.department Electrical and Computer Engineering en_US
dc.description.degree MS en_US

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search VTechWorks

Advanced Search


My Account