A many-valued logic with imperative semantics for incremental specification of timed models

Abstract

In order to reconcile the state of the art and the state of the practice in software engineering, immediate goals aim to use formal methods in ways that are minimally disruptive to professional practice. In this pursuit formal methods should be adapted to flexible lifecycle structures, getting over more traditional approaches. In the field of real-time design, SCTL/MUS-T methodology proposes a software process using formal methods that builds incrementally the model-oriented specification of the intended system. There are two main issues in this proposal: the incremental nature of the process, calling for a many-valued understanding of the world; and the construction of a model-oriented specification, calling for an imperative viewpoint in specification. From this starting point, this paper introduces a many-valued logic with imperative semantics enabling (1) to build a very-abstract level prototype from the scenarios identified on the intended system; (2) to capture the uncertainty and disagreement in an incremental process by providing a measure of how far or how close the prototype is from satisfying the intended requirements. © Springer-Verlag 2004.