Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
The Metrô Rio case study
Ferrari A., Fantechi A., Magnani G., Grasso D., Tempestini M. Science of Computer Programming78 (7):828-842,2013.Type:Article
Date Reviewed: Jun 16 2014

Seaplane and railway systems require reliable, smart machines for inevitably circumnavigating disasters and providing safety. How should formal models for the design, execution, and verification of automatic protection devices be developed? A robust system evolves from a model that captures its requirements to support reasoning about it, enables the precise specifications of its requirements, and supports the verification of correctness of its program design. Ferrari et al. present formal exemplar models for incorporating spontaneous safeguard detection features into the onboard equipment of complex systems such as trains, aircraft, and ships. The reader who is not acquainted with formal methods should browse the concepts in van Vliet’s book [1] prior to reading the perceptive ideas in this paper. A more detailed description of software cost reduction is also available in the literature [2].

An archetype two-phase strategy is proposed for reducing the cost of verifying the safety of automotive standards. The first phase uses a test model to validate the control flows and functional attributes of the components of a complex system. The second phase applies the theory of abstract machines to manually certify the data flow properties within an entire multifaceted system. The authors scrutinize the familiar Simulink Design Verifier as a functional unit testing tool to augment the formal verification of safety-critical systems. They use the Metrô Rio automatic train protection (ATP) system to illuminate the various concepts of formal methods for reliably designing, implementing, and verifying railway signaling systems.

In the Metrô Rio ATP system, encoders and transponders situated near train signals code and pass on telegram data to receiving instruments that process and impose speed limits within the distances of signals. The authors delineate system functions such as speed analyzers, speed limit manager, and brake manager as internal components. They define external components as software drivers that enable external devices, such as a tachometer and a braking tool to interface with the Metrô Rio ATP system. Unified modeling language (UML) diagrams were derived for the independent functioning units of the Metrô Rio ATP system, to provide a structural design of its units for a conversion into the Simulink construction, to reinforce unit requirements as state-flow finite automata, and to enable the safe code synthesis of the state-flow models of the functioning units.

The authors provide great insights into the formal design and verification of the individual components of a complex system. They creatively illuminate the processes of disintegrating and formalizing unit requirements. They provide a useful software correctness verification framework for ascertaining the practical consistency between software model and behavior. The test results derived from an ad hoc train simulation experiment are reliable enough to recommend the formal methods in this paper. As shown in the paper, the Simulink Design Verifier is a valuable tool for establishing the formal verification of the unit requirements of complex systems.

Reviewer:  Amos Olagunju Review #: CR142401 (1409-0760)
1) van Vliet, H. Software engineering: principles and practice (2nd ed.). John Wiley & Sons, New York, NY, 2000.
2) Heitmeyer, C. L.; Jeffords, R. D.; Labaw, B. G. Automated consistency checking of requirements specifications. ACM Transactions on Software Engineering and Methodology 5, 3(1996), 231–261.
Bookmark and Share
  Featured Reviewer  
 
Formal Methods (D.2.4 ... )
 
 
Code Generation (D.3.4 ... )
 
 
Model Development (I.6.5 )
 
Would you recommend this review?
yes
no
Other reviews under "Formal Methods": Date
On a method of multiprogramming
Feijen W., van Gasteren A., Springer-Verlag New York, Inc., New York, NY, 1999. Type: Book (9780387988702)
May 1 2000
Computer-Aided reasoning: ACL2 case studies
Kaufmann M. (ed), Manolios P. (ed), Moore J. Kluwer Academic Publishers, Norwell, MA,2000. Type: Divisible Book
Jul 2 2002
Architecting families of software systems with process algebras
Bernardo M., Ciancarini P., Donatiello L. ACM Transactions on Software Engineering and Methodology 11(4): 386-426, 2002. Type: Article
Mar 10 2003
more...

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