Step by Step to Histories
The behavior of reactive systems is typically specified by state machines. This results in an operational description of how a system produces its output. An alternative and more abstract approach is to just specify the relation between the input and output histories of a system. In this work, we propose a way to combine state-based and history-based specifications: Abstract communication history properties of system components can be derived from temporal logic properties of state machines. The history properties can then be used to deduce global properties of a complete system.