An effective means for analyzing and reasoning on software systems is to use formal specifications to simulate their execution. The simulation traces can be used for specification testing and reused for functional testing of the system later in the development process. It is widely acknowledged that, to deal with the complexity of industrial-size systems, specifications must be structured into modules providing abstraction mechanisms and clear interfaces. In our past work, we defined and implemented a method for simulating specifications written in the TRIO temporal logic language, and applied it to functional testing of time-critical industrial systems. In the present paper, we report on a tool that analyzes TRIO specifications by taking advantage of their modular structure, so as to overcome the well-known state-explosion problem and make the proposed method really scalable. We discuss the fundamental operations and the algorithms on which the tool is based. Then, we illustrate its use in a realistic case study, inspired by an industrial application. Finally, we comment on the overall results in terms of usability of the tool and effectiveness of the approach, and we suggest some future improvements.
A Case Study on Applying a Tool for Automated System Analysis Based on Modular Specifications Written in TRIO
MORASCA, SANDRO;MORZENTI, ANGELO CARLO;SAN PIETRO, PIERLUIGI
2000-01-01
Abstract
An effective means for analyzing and reasoning on software systems is to use formal specifications to simulate their execution. The simulation traces can be used for specification testing and reused for functional testing of the system later in the development process. It is widely acknowledged that, to deal with the complexity of industrial-size systems, specifications must be structured into modules providing abstraction mechanisms and clear interfaces. In our past work, we defined and implemented a method for simulating specifications written in the TRIO temporal logic language, and applied it to functional testing of time-critical industrial systems. In the present paper, we report on a tool that analyzes TRIO specifications by taking advantage of their modular structure, so as to overcome the well-known state-explosion problem and make the proposed method really scalable. We discuss the fundamental operations and the algorithms on which the tool is based. Then, we illustrate its use in a realistic case study, inspired by an industrial application. Finally, we comment on the overall results in terms of usability of the tool and effectiveness of the approach, and we suggest some future improvements.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
