The authors propose to study the requirements of time- and safety-critical systems via the use of automated deductive analysis. Their method is supported not only by a formal framework, but also by a working tool set. The temporal logic language TRIO is used as the underlying model. The proposal is illustrated by a general railroad crossing problem.
The paper is well written and readable. It is significant in several ways: from the theoretical perspective, the paper formalizes intuitive notions such as point- and interval-based predicates, non-Zeno requirements, periodic and semi-periodic events, and temporal and causal relations. In terms of technical contributions, the framework has been realized as a tool set inside a theorem prover. This supports the encoding of the logic, proof strategies for reasoning, and a “pretty printer” for visualization. In terms of methodology, the framework is supported by a predefined set of constructs and tools, and thus strongly encourages reuse.
Since the framework has been designed with a view to supporting system requirements analysis in real-life industrial applications, it would be useful if the deductive system could be coupled with a popular graphical user-interface such as the Unified Modeling Language (UML). For instance, instead of specifying in a formal language, the authors could consider enhancing UML to deal with non-functional properties, as well as advanced relations, such as compatibility and mutual exclusion. In this way, time- and safety-critical systems could be defined in a language that has a UML-like syntax, and yet contains a rich formal semantics like the one presented in the paper.