MODEL CHECKING OF COMPONENT BASED SOFTWARE USING COMPOSITIONAL REDUCTIONS

2008 ◽  
Vol 18 (05) ◽  
pp. 683-712 ◽  
Author(s):  
MOHAMMAD IZADI ◽  
ALI MOVAGHAR
Keyword(s):  
Model Checking ◽  
Composition Operators ◽  
Linear Time ◽  
Operational Semantics ◽  
Computing System ◽  
Transition System ◽  
Compositional Model ◽  
Temporal Properties ◽  
Labeled Transition System ◽  
Constraint Automata

A component-based computing system consists of two main parts: a set of components and a coordination subsystem. Reo is an exogenous coordination language for compositional construction of the coordination subsystem. Constraint automaton has been defined as the operational semantics of Reo. The main goal of this paper is to prepare a model checking method for verifying linear time temporal properties of component-based systems whose coordinating subsystems are modeled by Reo and components are modeled by labeled transition systems. For this purpose, we introduce modified definitions of constraint automata and their composition operators by which, every constraint automaton can be considered as a labeled transition system and each labeled transition system can be translated into a constraint automaton. We show that failure-based equivalences CFFD and NDFD are congruences with respect to the composition operators of constraint automata. Also we present a method for compositional model checking of component-based systems using these equivalences for reducing the sizes of constraint automata models.

scholarly journals Model-checking the Preservation of Temporal Properties upon Feature Integration

2005 ◽  
Vol 128 (6) ◽  
pp. 311-324 ◽  
Author(s):  
Dimitar P. Guelev ◽  
Mark Ryan ◽  
Pierre Yves Schobbens
Keyword(s):  
Model Checking ◽  
Feature Integration ◽  
Temporal Properties

AN OPERATIONAL SEMANTICS FOR THE PARALLEL LANGUAGE EDEN

2002 ◽  
Vol 12 (02) ◽  
pp. 211-228 ◽  
Author(s):  
MERCEDES HIDALGO-HERRERO ◽  
YOLANDA ORTEGA-MALLÉN
Keyword(s):  
Operational Semantics ◽  
Transition System ◽  
Lazy Evaluation ◽  
Parallel Language ◽  
Parallel Processes ◽  
System A ◽  
Independent Evaluation ◽  
Level Transition ◽  
Concurrent Algorithms ◽  
Main Thread

The functional parallel language Eden — suitable for the description of parallel and concurrent algorithms in a distributed setting — is an extension of Haskell with a set of coordination features. In this paper we present a formal operational semantics for the kernel of Eden, or more precisely, for a λ-calculus widened with explicit parallelism and potentially infinite communication channels. Eden overrides the lazy nature of Haskell on behalf of parallelism. This interplay between laziness and eagerness is accurately described by the semantics proposed here, which is based on Launchbury's natural semantics for lazy evaluation, and is expressed through a two-level transition system: a lower level for the local and independent evaluation of each process, and an upper one for the coordination between all the parallel processes in the system. As processes are created either under demand or in a speculative way, different scheduling strategies are possible — ranging from a minimal one that only allows the main thread to evolve, to a maximal one that evolves in parallel every active binding.

scholarly journals From Interpreter to Logic Engine by Defunctionalization

2003 ◽  
Vol 10 (25) ◽  
Author(s):  
Dariusz Biernacki ◽  
Olivier Danvy
Keyword(s):  
Logic Programming ◽  
Programming Language ◽  
Operational Semantics ◽  
Lambda Calculus ◽  
Transition System ◽  
Abstract Machine ◽  
Logic Programming Language ◽  
Delimited Continuations ◽  
Simple Logic ◽  
Control Operators

Starting from a continuation-based interpreter for a simple logic programming language, propositional Prolog with cut, we derive the corresponding logic engine in the form of an abstract machine. The derivation originates in previous work (our article at PPDP 2003) where it was applied to the lambda-calculus. The key transformation here is Reynolds's defunctionalization that transforms a tail-recursive, continuation-passing interpreter into a transition system, i.e., an abstract machine. Similar denotational and operational semantics were studied by de Bruin and de Vink in previous work (their article at TAPSOFT 1989), and we compare their study with our derivation. Additionally, we present a direct-style interpreter of propositional Prolog expressed with control operators for delimited continuations.<br /><br />Superseded by BRICS-RS-04-5.

Service Discovery and Composition Based on Contracts and Choreographic Descriptions

2012 ◽  
pp. 60-88
Author(s):  
Mario Bravetti ◽  
Gianluigi Zavattaro
Keyword(s):  
Service Discovery ◽  
Operational Semantics ◽  
Asynchronous Communication ◽  
Synchronous Communication ◽  
Transition Systems ◽  
Service Contracts ◽  
Contract Compliance ◽  
Service Oriented ◽  
Labeled Transition System ◽  
Contract Language

The authors discuss the interplay between the notions of contract compliance, contract refinement, and choreography conformance in the context of service oriented computing, by considering both synchronous and asynchronous communication. Service contracts are specified in a language independent way by means of finite labeled transition systems. In this way, the theory is general and foundational as the authors abstract away from the syntax of contracts and simply assume that a contract language has an operational semantics defined in terms of a labeled transition system. The chapter makes a comparative analysis of synchronous and asynchronous communication. Concerning the latter, a realistic scenario is considered in which services are endowed with queues used to store the received messages. In the simpler context of synchronous communication, the authors are able to resort to the theory of fair testing to provide decidability results.

Sign in / Sign up

Export Citation Format

Share Document