Real-Time Software Development with Formal Models

Abstract

Improvements in microprocessor technology have prompted a willingness to embed computer hardware in structural and mechanical systems. Active structural control is one such application in which computer-based sensors and actuators work to limit vibrations and reduce the possibility of failure in seismic events. Although there have been numerous studies on control strategies for these real-time systems, our goal is to develop approaches that can ensure the overall reliability of the software before deployment. In this paper, we outline a three-step approach based on formal methods for designing reliable real-time systems. This approach includes an analysis of the required timing properties, a modeling technique based on real-time logic and Modechart, and a verification procedure using simulation and model checking. As demonstrated with an application to structural control, this process ensures that the necessary timing properties are satisfied by a given hardware and software architecture.