Abstract
In this paper, we describe a true-concurrent hierarchical logic interpreted over concurrent automata. Concurrent automata constitute a special kind of asynchronous transition system (ATS) used for modelling the behaviour of components as understood in component-based software development. Here, a component-based system consists of several interacting components whereby each component manages calls to and from the component using ports to ensure encapsulation. Further, a component can be complex and made of several simpler interacting components. When a complex component receives a request through one of its ports, the port delegates the request to an internal component. Our logic allows us to describe the different views we can have on the system. For example, the overall component interactions, whether they occur sequentially, simultaneously or in parallel, and how each component internally manages the received requests (possibly expressed at different levels of detail). Using concurrent automata as an underlying formalism we guarantee that the expressiveness of the logic is preserved in the model. In future work, we plan to integrate our truly-concurrent approach into the Edinburgh Concurrency Workbench. © 2007 Elsevier B.V. All rights reserved.