This paper presents the TRIO logical framework to specify industrial real-time systems. Typical specification requirements for this kind of system are discussed and related to corresponding features of the framework. In particular, the methodological expressiveness, the validation and the temporal constraint proof capabilities are highlighted. The former is mainly dealt with by the Object Oriented paradigm, while the latter is dealt with by a formal method specification derived from Metric Temporal Logic languages. Further, this Metric Temporal Logic is extended with the ability to treat different granularities. In order to show the capabilities of the TRIO logical framework, the specification of a complex real-time system is proposed.
An MILP approach for real-time optimal controller synthesis with Metric Temporal Logic specifications
