Model-based Systems Architecting

Appendix 1System Temporal Logic

Formal requirements are expressed in system temporal logic¹, a mathematical formalism that we did not present below and that we will discuss in full details in this appendix.

System temporal logic is a formal logic that extends the same classical notion for computer programs (see for instance Pnueli 1977; Manna and Pnueli 1992; Baier and Katoen 2008; Kröger and Merz 2008; Katoen 2009; Murray 2012; Artale 2010-2011). Such a logic intends to specify the sequences of input/output and internal variable observations that can be made on a formal system whose input, output and internal variable sets X, Y, Q and timescale T are fixed. In other terms, system temporal logic specifies the sequences O of values of inputs, outputs and internal variables that can be observed among all moments of time t within the timescale T, as stated below:

O = (O(t)) for all t ∈ T, where we set O(t) = (x(t), y(t), q(t))².

It is based on the atomic formulae that may be either “TRUE” or equal to O(x, y, q)³, where x (resp. y or q) is either an element of the input set X (resp. output set Y or internal variable set Q) or equal to the special symbol ∅ (that models an arbitrary value), except that x, y and q cannot be all equal to ∅. Atomic formulae within system temporal logic are the following:

[A1.1]

System temporal logic will then manipulate logical formulae – that is, well-formed ...