ABD 2: Languages & Tools for probabilistic & Temporal specifications
D. Borrione · Forum on specification and Design Languages · 2012
The first paper defines a variation of bounded LTL, and its trace semantics, for the specification of reliability requirements for embedded systems; action traces are processed to compute the reliability satisfaction for a given action schedule. The second (invited) paper is an introduction to the MODEST specification language and its toolset.