Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Automated deductive requirements analysis of critical systems
Gargantini A., Morzenti A. ACM Transactions on Software Engineering and Methodology10 (3):255-307,2001.Type:Article
Date Reviewed: May 9 2002

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.

Reviewer:  T.H. Tse Review #: CR125923 (0205-0270)
Bookmark and Share
Methodologies (D.2.1 ... )
Formal Methods (D.2.4 ... )
Real-Time And Embedded Systems (C.3 ... )
Model Validation And Analysis (I.6.4 )
Special-Purpose And Application-Based Systems (C.3 )
Would you recommend this review?
Other reviews under "Methodologies": Date
Multilevel specification of real time systems
Gabrielian A., Franklin M. Communications of the ACM 34(5): 50-60, 1991. Type: Article
May 1 1992
Software requirements
Davis A., Prentice-Hall, Inc., Upper Saddle River, NJ, 1993. Type: Book (9780138057633)
Nov 1 1994
The automated production control documentation system
Trammell C., Binder L., Snyder C. ACM Transactions on Software Engineering and Methodology 1(1): 81-94, 1992. Type: Article
Mar 1 1993

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2023 ThinkLoud®
Terms of Use
| Privacy Policy