Title page for ETD etd-05102004-195753


Type of Document Master's Thesis
Author Suhaib, Syed Mohammed
Author's Email Address ssuhaib@vt.edu
URN etd-05102004-195753
Title XFM: An Incremental Methodology for Developing Formal Models
Degree Master of Science
Department Electrical and Computer Engineering
Advisory Committee
Advisor Name Title
Shukla, Sandeep K. Committee Chair
Ha, Dong Sam Committee Member
Ravindran, Binoy Committee Member
Keywords
  • Formal Verification
  • SPIN
  • SMV
  • Embedded Systems
  • Property Refactoring
  • Prescriptive Formal Models
  • Extreme Modeling
  • Property Ordering
  • Extreme Programming
Date of Defense 2004-05-06
Availability unrestricted
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.
Files
  Filename       Size       Approximate Download Time (Hours:Minutes:Seconds) 
 
 28.8 Modem   56K Modem   ISDN (64 Kb)   ISDN (128 Kb)   Higher-speed Access 
  suhaib_thesis.pdf 628.39 Kb 00:02:54 00:01:29 00:01:18 00:00:39 00:00:03

Browse All Available ETDs by ( Author | Department )

dla home
etds imagebase journals news ereserve special collections
virgnia tech home contact dla university libraries

If you have questions or technical problems, please Contact DLA.