Show simple item record

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.rightsI hereby certify that, if appropriate, I have obtained and attached hereto a written permission statement from the owner(s) of each third party copyrighted matter to be included in my thesis, dissertation, or project report, allowing distribution as specified below. I certify that the version I submitted is the same as that approved by my advisory committee. I hereby grant to Virginia Tech or its agents the non-exclusive license to archive and make accessible, under the conditions specified below, my thesis, dissertation, or project report in whole or in part in all forms of media, now or hereafter known. I retain all other ownership rights to the copyright of the thesis, dissertation or project report. I also retain the right to use in future works (such as articles or books) all or part of this thesis, dissertation, or project report.en_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.degreeMaster of Scienceen_US
thesis.degree.nameMaster of Scienceen_US
thesis.degree.levelmastersen_US
thesis.degree.grantorVirginia Polytechnic Institute and State Universityen_US
thesis.degree.disciplineElectrical and Computer Engineeringen_US
dc.contributor.committeechairShukla, Sandeep K.en_US
dc.contributor.committeememberRavindran, Binoyen_US
dc.contributor.committeememberHa, Dong Samen_US
dc.identifier.sourceurlhttp://scholar.lib.vt.edu/theses/available/etd-05102004-195753en_US
dc.date.sdate2004-05-10en_US
dc.date.rdate2004-05-13
dc.date.adate2004-05-13en_US


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record