Specifying and Verifying External Behaviour of Fair Input/Output Automata by Using the Temporal Logic of Actions

Fair input/output (or I/O) automata are a state-machine model for specifying and verifying reactive and concurrent systems. For the verification purposes, one is usually interested only in the sequences of interactions fair I/O automata offer to their environment. These sequences are called fair traces. The usual approach to the verification consists in proving fair trace inclusion between fair I/O automata. This paper presents a simple approach to the specification of fair traces and shows how to establish a fair trace inclusion relation for a pair of fair I/O automata by using the temporal logic of actions. Key words: formal specification, fair input/output automaton, temporal logic of actions, fair trace, fair trace inclusion.

• Type: Journal
• Year: 2016
• Where: INFORMATICALT
• Authors: Tatjana Kapus
• Keywords: INFORMATICALT 2016, Software Engineering