MS Plan-B Project Description

Title - Integration of the VDM-SL Toolbox and the Nimbus Environment
The project involves the integration of two formal modeling tools, the VDM-SL toolbox and the Nimbus environment for RSML-e. Both tools allow the communication with external tools; thus, integration should be straight forward. The integration must be demonstrated with smaller examples. 

Duration
Desired completion date: End of summer 2001. 

Skills Required
Experience with C++ and C is required. Experience with formal modeling in VDM-SL is desirable, but not required.  

Project Description
Our research group has developed a formal specification language called RSML-e (Requirements State Machine Language without events) suitable for the modeling of safety critical systems. The language is supported with an execution environment we call Nimbus. 

RSML-e is based on finite state machines and is suitable for modeling a certain class of  systems--reactive systems. RSML-e is not particularly well suited for the modeling of systems that involve keeping track of sequences or sets of data. Other formal modeling languages, for example, VDM-SL, are based on set theory and are well suited for modeling of sequences and sets. To take advantage of the strengths of the various languages, while at the same time circumvent the weaknesses, we want to be able to model parts of a system in RSML-e and other parts in VDM-SL. Therefore, we want to integrate the execution environments for the two languages so that we can simulate a system as a whole. 

Both execution environments support integration with external tools; thus, for the experienced C++ and C programmer, the integration should be straight forward. The integration must be demonstrated with a few examples illustrating how the tool integration is used. 

Preparatory Readings
  • Modelling Systems: Practical Tools and Techniques in Software Development. John Fitzgerald and Peter Gorm Larsen. Cambridge University Press, 1998. ISBN 0-521-62348-0
  • Information on VDM-SL is also available from the IFAD website here.
  • J.M. Thompson, M.P.E. Heimdahl, and S.P. Miller. Specification-Based Prototyping for Embedded Systems. Proceedings of the Seventh ACM/SIGSOFT Symposium on the Foundations of Software Engineering, Toulouse, France, September, 1999. [Postscript] [PDF]
  • J.M. Thompson, M.P.E. Heimdahl, and D.M. Erickson. Structuring formal control systems specifications for reuse: Surviving hardware changes. In the Fifth NASA Langley Formal Methods Workshop (LFM 2000), June 2000. [Postscript] [PDF]

 

Skills Acquired
The project will provide experience advanced software engineering techniques (OO programming, OO patterns, formal modeling in RSML-e and VDM-SL). Some results of the project may be publishable.

The views and opinions expressed in this page are strictly those of the page author.
The contents of this page have not been reviewed or approved by the University of Minnesota.