Specification
CLIMB adopts extended DecSerFlow/Condec as graphical high-level specification languages, and
SCIFF as their underlying semantics, avoiding both over-specification and over-constraining
issues.
In particular, a complete mapping of core DecSerFlow/Condec constraints has been given in terms of
SCIFF rules.
SCIFF defines a rule-based language for the specification of interaction with a clear declarative
semantics as well as a proof-theoretic operational counterpart able to verify (at run-time or
a-posteriori) whether a concrete execution complies with the prescribed rules. The proof-procedure has
been extended to deal also with static verification of properties and interoperability verification.
A CLIMB model is therefore a SCIFF specification which maps an extended DecSerFlow model.
DecSerFlow/ConDec
DecSerFlow and Condec are a family of graphical languages for the declarative specification of service/
business flow. Instead of focusing on a specific procedural solution, they model service interaction
and processes by specifying the (minimal) set of constraints among messages/activities.
In this way, they overcome both over-specification and over-constraining issues, supporting the
development of loosely-coupled and flexible models. Such an approach is particularly suitable to model
service choreographies.
The SCIFF Language
SCIFF specifies interaction by adopting a declarative and open approach. Interacting entities are considered as members of an open society; they are not known a-priori and can be heterogeneous: the only first-class entities in SCIFF are the observable and relevant events which occur during execution. Such events are constrained by means of Integrity Constraints, forward reactive rules that specify which expectations about the course of interaction are generated, from the global "social" viewpoint, when some events happen. Happened events and expectations come respectively with form H(Event, T) (Event is happened at time T) and E/EN(Event, T) (Event is expected to happen /not to happen at time T). Events are terms and can contain variables. All variables (times included) can be constrained by means of Prolog predicates and CLP constraints. The latter are typically used to quantitatively constrain execution times and express deadlines/delays.