University of Minnesota
Software Engineering Center

You are here

Structuring Formal Control Systems Specifications for Reuse: Surviving Hardware Changes

Date of Publication: 
January 2000
Associated Research Groups: 
Publication Files: 
Formal capture and analysis of the required behavior of control systems have many advantages. For instance, it encourages rigorous requirements analysis, the required behavior is unambiguously defined, and we can assure that various safety properties are satisfied. Formal modeling is, however, a costly and time consuming process and if one could reuse the formal models over a family of products, significant cost savings would be realized. In an ongoing project we are investigating how to structure state-based models to achieve a high level of reusability within product families. In this paper we discuss a high-level structure of requirements models that achieves reusability of the desired control behavior across varying hardware platforms in a product family. The structuring approach is demonstrated through a case study in the mobile robotics domain where the desired robot behavior is reused on two diverse platforms---one commercial mobile platform and one build in-house. We use our language rsml to capture the control behavior for reuse and our tool nimbus to demonstrate how the formal specification can be validated and used as a prototype on the two platforms.
Fifth NASA Langley Formal Methods Workshop, Virginia, January 2000
@TechReport{Thompson00:hardware-reuse-tech-report, author = {Jeffrey M. Thompson and Mats P.E. Heimdahl and Debra M. Erickson}, title = {Structuring Formal Control Systems Specifications for Reuse: Surviving Hardware Changes}, institution = {University of Minnesota}, year = {2000}, number = {TR 00-004}, month = {January}, note = {Submitted to the {\em Fifth NASA Langley Formal Methods Workshop}} }