Behavioral specification of reactive systems using stream-based I/O tables

摘要

A core problem in formal methods is the transition from informal requirements to formal specifications. Espe-cially when specifying the behavior of reactive systems, many formalisms require the user to either understand a com-plex mathematical theory and notation or to derive details not given in the requirements, such as the state space of the problem. For many approaches also a consistent set of requirements is needed, which enforces to resolve require-ments conflicts prior to formalization. This paper describes a specification technique, where not states but signal patterns are the main elements. The notation is based on tables of regular expressions and supports a piece-wise formalization of potentially inconsistent requirements. Many properties, such as input completeness and consistency, can be checked automatically for these specifications. The detection and res-olution of conflicts can be performed within our framework after formalization. Besides the formal foundation of our approach, this paper presents prototypical tool support and results from an industrial case study.