Constraint automata have been used as an operational model for component connectors described in the coordination language Reo which specifies the cooperation and communication of...
Dcpos can be presented by a preorder of generators and inequational relations expressed as covers. Algebraic operations on the generators (possibly with their results being ideals...
In the previous, companion, paper [13] to this paper we introduced our general model of refinement, discussed ideas around determinism and interfaces that the general definition r...
Petri nets are a formalism for modelling and validating critical systems. Generally, the approach to specification starts from an abstract view of the system under study. Once val...
We introduce a general model of refinement. This is defined in terms of what contexts an entity can appear in, and what observations can be made of it in those contexts. We show e...
Circus is a refinement language, in which specifications define both data and behavioural aspects of concurrent systems using a combination of Z and CSP. Its refinement theory and...
The Event-B method is a formal approach to modelling systems, using refinement. Initial specification is a high level of abstraction; detail is added in refinement steps as the de...
Several recent research efforts have focused on the dynamic aspects of software architectures providing suitable models and techniques for handling the run-time modification of th...
Roberto Bruni, Antonio Bucchiarone, Stefania Gnesi...