AN OBJECT-ORIENTED LOGIC LANGUAGE FOR MODULAR SYSTEM SPECIFICATION

We define TRIO+, an Object Oriented logic language for modular system specification. TRIO+ is based on TRIO, a first order modal language that is well suited to the specification of embedded and real-time systems, and provides an effective support to a variety of validation activities, like specification testing, simulation, and property proof. Unfortunately, TRIO lacks the possibility to construct specifications of complex systems in a systematic and modular way. TRIO+ combines the use of constructs for hierarchical system decomposition, and object oriented concepts like inheritance and genericity, with an expressive and intuitive graphic notation, yielding a specification language that is formal and rigorous, and still flexible, readable, general, and easily adaptable to the user's needs.