Español(Spanish Formal International)English (United Kingdom)
ACSL Specification, Semantic Verification and Evaluation

The definition of an XML grammar for ACSL by means of the XML Schema formalism can only validate the IP specifications syntactically. To be able to validate and evaluate these specifications semantically, the ACSL language also needs to be furnished with formal and operational semantics that can unambiguously describe the dynamic meaning of its syntactic constructs. The features of ACSL have led to the use of the concept of Structural Operational Semantics (SOS) [4, 3] as an approach for specifying the dynamic meaning of IPs. The dynamic meaning of a protocol is obtained from the dynamic meaning of the different syntactic constructs that appear in its specification. It covers the execution of the specification, including expression evaluation, message sending and reception and the execution of other non-communicative actions. The SOS denotes a formalism that can specify the meaning of a language by means of syntactic transformations of the programs or specifications written in this language. Some special points had to be taken into account to apply the SOS formalism, designed for programming languages, to a specification language such as ACSL. The definition of operational semantics suited for ACSL was a three-step process:

  1. Definition of a terminal and labeled transitional term-rewriting system based on the operational semantics described in [2],
  2. Definition of the interpreter I for this system, as proposed in [4], whose behavior is specified by a set of production rules. I is modeled as a function whose argument is a protocol P specified in ACSL in an environment w, and describes the behavior of (P,w) as an (in)finite series of productions like (P.w)->(P1,w1)->(P2,w2)->... If P ends, then the result is (END,wn).
  3. Process of outputting the interpreter for each ACSL construct.

The provision of formal semantics for ACSL means that the IP specification can be analyzed to find out whether the IP has certain properties, such as termination in finite time, conversational state reachability or no deadlocks and starvations. On the other hand, the provision of operational semantics makes it possible to automatically derive IP implementation from protocol specification, easing its simulation and the automatic generation of proxies that assure that each participant effectively complies with the protocol rules and provides assistance for protocol machine learning. The details of this view are described in the following subsections, each of whom is devoted to a different step of the ACSL operational semantics definition process.

Se ponen links a páginas que contengan las reglas para los protocolos listados (Sian e IteratedContractNet). Pueden ser PDFs o JPGs por lo complejo de la notación.

© CoNWeT Lab. 2008-2009.