Formal Modelling of Reactive Hardware/software Systems

The inherent complexity of modern reactive hardware/software systems requires the creation of system models before these systems are actually being built. A system model must allow a designer to reason about the essential properties of the system at the right level of abstraction. Therefore these models must be expressed in a formal language that is able to express these properties and that allows them to be examined by automated tools. In this paper we introduce a new systemlevel specification language called POOSL (Parallel Object-Oriented Specification Language). The key feature of the language is the expressive power to model very complex dynamic (communication and functional) behaviour as well as static (architecture and topology) structure in an object-oriented fashion. The language integrates a process part, based on the process algebra CCS, with a data part, based on the concepts of traditional object-oriented programming languages. Unlike many modelling languages today, POOSL ..