Step by Step to Histories

The behavior of reactive systems is typically speci ed by state machines. This results in an operational description of how a system 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 speci cations: 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.

• Type: Conference
• Year: 2000
• Where: AMAST
• Authors: Max Breitling, Jan Philipps
• Keywords: AMAST 2000, History Properties, Software Engineering, State Machines, Temporal Logic Properties