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.

Object-oriented logical specification of time-critical systems

MORZENTI, ANGELO CARLO;SAN PIETRO, PIERLUIGI
1994-01-01

Abstract

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.
1994
First-order logic; formal speclficatlons; model-theoretic semantics; object-oriented methodologies; real-time systems; temporal logic
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11311/666190
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact