Specifying, validating, and testing a traffic management system in the TRIO environment

Reports on an experience in applying a formal method to the specification and design of a system for monitoring and controlling surface vehicle traffic in a densely populated urban area. This method is based on TRIO, a linear time metric temporal logic, and includes a series of software tools providing (with various degrees of automation) support to the crucial activities of the system development. We illustrate the goals of the experience and describe the specification, validation and verification activities. We also discuss the problems deriving from the particular but (under several aspects) typical history of the application development, and from applying formal methods in an industrial setting. Finally, we assess the encouraging results obtained in the project.