Cumulating constraints on the 'when' and the 'what'

A graphical notation is presented for specifying the behaviour of a concurrent system according to an extensional, constraint-oriented approach. The behaviour is modelled by a set of states and events, labelled by variables. The notation represents explicitly states, events, constraints on state/event values (the 'WHAT') and constraints on the temporal ordering of the events (the 'WHEN'); it supports declarativity, cumulation of constraints into graphs, encapsulation of systems of constraints into views, and view composition. Specifications can be developed in a natural, incremental and modular, way. This research is mainly motivated by the need to enhance the expressive immediacy and flexibility offered by other widely used specification languages (individually), in particular LOTOS, Z and Petri Nets, and to integrate some of their best features into a unique framework. The formal semantics for the notation without hierarchy is sketched, and a non trivial example of specification is provided.