Object-oriented logical specification of time-critical systems

We define TRIO+, an object-oriented logical language for modular system specification, TRIO+ is based on TRIO, a first-order temporal language that 1s well smted to the specification of embedded and real-time systems, and that provides an effective support to a variety of validation activities, like specification testing, slmulatlon, and property proof. Unfortunately, TRIO lacks the abihty to construct specifications of complex systems m a systematic and modular way, TRIO + combmes the use of constructs for hierarchical system decomposition and object-oriented concepts like inheritance and genericlty with an expressive and intuitive graphic notation, yielding a specification language that M formal and rigorous, yet still flexlble, readable, general, and easdy adaptable to the user’s needs. After introducing and motlvatmg the mam features of the language, we Illustrate its apphcation to a nontrivial case study extracted from a real-life industrial application