We introduce a simple conceptual framework for assessing a number of well known formal specification techniques w.r.t. their ability to model state-oriented and/or event-oriented aspects of system behaviour. By attributing a-priori equal importance to the notions of event and state, by explicitly recognizing the two derived, fundamental ways of thinking about system behaviours, and by assessing the bias of existing formal methods towards one or the other, one can make more conscious choices in the upper phases of software development, that is, in requirements elicitation and analysis, in the construction of abstract system models, and in the choice of formal languages for high- and low-level design. In particular, we assess the recently introduced model of abstract state processes, and the design choices behind its definition, in light of the introduced state-event framework.

In this paper, we propose to conservatively extend object-oriented decomposition by letting it affect also operations (methods). Different objects may support different parts of the same operation. The responsibility of defining an operation, in terms of enabling conditions and effects on the state, is distributed over several interacting objects, which act as constraints and express different, partial views about the system behavior. Constraint-oriented reasoning has already been explored and applied in the context of formal specification languages for concurrent and reactive systems, and is sufficiently different from object-oriented reasoning to be considered as a paradigm in itself, with its own specific advantages. Nevertheless, the paper shows that the two approaches are sufficiently compatible to be profitably integrated. We introduce a constraint-oriented style for an object-oriented programming language (JAVA).

We propose an enrichment of the Prolog language based on the introduction of explicit notions of state variables and, most notably, of actions. The extended language, called co-notation, supports the formal, executable description of a wide variety of systems in a so-called ‘constraint-oriented style’: system behaviours are described as hierarchical compositions of constraints on actions and state variables. Elementary constraints include state invariants, referring to one or more state variables, and ‘active predicates’, involving one action and zero or more state variables. Compound constraints are encapsulated compositions of elementary and/or compound constraints, and represent partial views about the system behaviour. Constraint composition is also reminiscent of process composition in process algebra, but encompasses interaction both by rendez-vous and by shared variables. © 1998 John Wiley & Sons, Ltd.

We illustrate the expressive flexibility of the ‘co-notation’, a declarative, structured, constraint-oriented specification technique for concurrent systems where constraints on actions and on data variables are intertwined. Flexibility is intended here as the ability to closely match the structure of the initial, informal behavioural description of the system, and to directly formalize the conceptual links among data variables and events, and their groupings, as expressed in that description. We contrast the co-notation with two related and ‘mature’ specification techniques, namely predicate/transition Petri nets and LOTOS, also by means of a running example. The Petri net approach supports a quite direct specification of the links among actions and data variables, but it lacks structuring facilities; LOTOS does support encapsulation, but its process-oriented view does not offer full flexibility in defining and composing groups of those conceptual links. We show that the simple yet powerful constraint conjunction operator of the co-notation, supporting both shared-action (rendez-vous) and shared-variable interaction mechanisms, achieves a higher expressive flexibility than the other models, and brings to a full exploitation the constraint-oriented reasoning partially offered by LOTOS.

An overview of some LOTOS (Language of Temporal Ordering Specification) constructs for expressing the behavior of distributed and concurrent systems is given. Some existing equivalent laws for LOTOS behavior expressions that involve the parallel composition operator and that are based on the notion of bisimulation equivalence are recalled. The graphical representation of the parallel composition of several LOTOS processes as a network of interconnected boxed is ambiguous. However, under sufficiently general conditions such graphical representation is sound; a method for deriving from any such graph a family of strongly equivalent LOTOS expressions that describe the intended process composition is introduced and proved correct. The method legitimizes the adoption of a graphical (or an equivalent textual) shorthand for such multiple compositions. It can be used for transforming the structure of parallel LOTOS expressions, and it is a generalization of previously known algebraic laws.>