Regresar

Incremental specification with SCTL/MUS-T: A case study

Abstract:

The past decade witnessed a great advance in the field of timed formal methods for the specification and analysis of real-time and safety-critical systems. In this context, timed automata and real-time temporal logics provide a simple, and yet general, way to model and specify the behavior of these systems. At the same time, iterative and incremental development has been massively adopted in professional practice. In order to get closer to this current trend, timed formal methods should be adapted to such lifecycle structures, getting over their traditional role of verifying that a model meets a set of fixed requirements. In the pursuit of this ultimate aim, we propose SCTL/MUS-T, a timed methodology in which many-valuedness let deal with both the uncertainty and the disagreement which are pervasive and desirable in an iterative and incremental process. To illustrate the main ideas behind SCTL/MUS-T methodology this paper focuses on the specification, synthesis and verification of the well known steam-boiler case study. © 2003 Elsevier Inc. All rights reserved.