Show simple item record

dc.contributor.advisorShukla, Sandeep K.en_US
dc.contributor.advisorRavindran, Binoyen_US
dc.contributor.advisorHa, Dong S.en_US
dc.contributor.authorSuhaib, Syed Mohammeden_US
dc.date.accessioned2011-08-06T16:01:28Z
dc.date.available2011-08-06T16:01:28Z
dc.date.issued2004-05-07en_US
dc.identifier.otheretd-05102004-195753en_US
dc.identifier.urihttp://hdl.handle.net/10919/9905
dc.description.abstractWe 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.mediumETDen_US
dc.publisherVirginia Techen_US
dc.relation.haspartsuhaib_thesis.pdfen_US
dc.rightsThe 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.urihttp://scholar.lib.vt.edu/theses/available/etd-05102004-195753en_US
dc.subjectFormal Verificationen_US
dc.subjectSPINen_US
dc.subjectSMVen_US
dc.subjectEmbedded Systemsen_US
dc.subjectProperty Refactoringen_US
dc.subjectPrescriptive Formal Modelsen_US
dc.subjectExtreme Modelingen_US
dc.subjectProperty Orderingen_US
dc.subjectExtreme Programmingen_US
dc.titleXFM: An Incremental Methodology for Developing Formal Modelsen_US
dc.typeThesisen_US
dc.contributor.departmentElectrical and Computer Engineeringen_US
dc.description.degreeMSen_US


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record