scholarly journals Model Checking Techniques applied to the design of Web Services

2007 ◽  
Vol 10 (2) ◽  
Author(s):  
Gregorio Dıaz ◽  
Emilia M. Cambronero ◽  
Juan J. Pardo ◽  
Valentın Valero ◽  
Fernando Cuartero
Keyword(s):  
Model Checking ◽  
Web Services ◽  
Timed Automata ◽  
Critical Role ◽  
Verification And Validation ◽  
Time Constraints ◽  
Model Checker

In previous work we have presented the generation of WS-CDL and WS-BPEL documents. In this paper we show the unification of both generations. The aim is to generate correct WS-BPEL skeleton documents from WS-CDL documents by using the Timed Automata as an intermediary model in order to check the correctness of the generated Web Services with Model Checking Techniques. The model checker used is UPPAAL, a well known tool in theoretical and industrial cases that performs the verification and validation of Timed Automata. Note that our interest is focused on Web services where the time constraints play a critical role.

scholarly journals Is your Model Checker on Time? On the Complexity of Model Checking for Timed Modal Logics

1999 ◽  
Vol 6 (32) ◽  
Author(s):  
Luca Aceto ◽  
Francois Laroussinie
Keyword(s):  
Computational Complexity ◽  
Model Checking ◽  
Timed Automata ◽  
Structural Complexity ◽  
Modal Logics ◽  
System Model ◽  
Model Checker ◽  
Program Complexity

This paper studies the structural complexity of model checking<br />for (variations on) the specification formalisms used in the tools CMC<br />and Uppaal, and fragments of a timed alternation-free mu-calculus. For<br />each of the logics we study, we characterize the computational complexity<br />of model checking, as well as its specification and program complexity,<br />using timed automata as our system model.

scholarly journals On Memory-Block Traversal Problems in Model Checking Timed Systems

2000 ◽  
Vol 7 (3) ◽  
Author(s):  
Fredrik Larsson ◽  
Paul Pettersson ◽  
Wang Yi
Keyword(s):  
Model Checking ◽  
State Space ◽  
Operating Systems ◽  
Memory Management ◽  
Timed Automata ◽  
Model Checker ◽  
Timed Systems ◽  
Memory Block ◽  
Start Up

A major problem in model-checking timed systems is the<br />huge memory requirement. In this paper, we study the memory-block<br />traversal problems of using standard operating systems in exploring the<br />state-space of timed automata. We report a case study which demonstrates<br />that deallocating memory blocks (i.e. memory-block traversal)<br />using standard memory management routines is extremely time-consuming.<br />The phenomenon is demonstrated in a number of experiments by<br />installing the Uppaal tool on Windows95, SunOS 5 and Linux. It seems<br />that the problem should be solved by implementing a memory manager<br />for the model-checker, which is a troublesome task as it is involved in<br />the underlining hardware and operating system. We present an alternative<br />technique that allows the model-checker to control the memory-block<br />traversal strategies of the operating systems without implementing<br />an independent memory manager. The technique is implemented in the<br />Uppaal model-checker. Our experiments demonstrate that it results in<br />significant improvement on the performance of Uppaal. For example, it<br />reduces the memory deallocation time in checking a start-up synchronisation<br />protocol on Linux from 7 days to about 1 hour. We show that the<br />technique can also be applied in speeding up re-traversals of explored<br />state-space.

From Implicit to Explicit Transitions in Business Protocols

2012 ◽  
Vol 9 (4) ◽  
pp. 69-95 ◽  
Author(s):  
Emad Elabd ◽  
Emmanuel Coquery ◽  
Mohand-Said Hacid
Keyword(s):  
Web Services ◽  
Web Service ◽  
Timed Automata ◽  
Automated Analysis ◽  
Time Constraints ◽  
Major Step ◽  
Modeling Tools ◽  
Business Protocols

Modeling Web services is a major step towards their automated analysis. One of the important parameters in this modeling, for the majority of Web services, is the time. A Web service can be presented by its behavior which can be described by a business protocol representing the possible sequences of message exchanges. To the best of the authors’ knowledge, automated analysis of timed Web services (e.g., compatibility and replaceability checking) is very difficult and in some cases it is not possible with the presence of implicit transitions (internal transitions) based on time constraints. The semantics of the implicit transitions is the source of this difficulty because most of well-known modeling tools do not express this semantics (e.g., epsilon transition on the timed automata has a different semantics). This paper presents an approach for converting any protocol containing implicit transitions to an equivalent one without implicit transitions before performing analysis.

Using Timed Automata for Modeling the Clocks of Distributed Embedded Systems

2010 ◽  
pp. 172-193 ◽  
Author(s):  
Guillermo Rodriguez-Navas ◽  
Julian Proenza ◽  
Hans Hansson ◽  
Paul Pettersson
Keyword(s):  
Model Checking ◽  
Embedded Systems ◽  
Embedded System ◽  
Timed Automata ◽  
Model Checker ◽  
Distributed Embedded Systems ◽  
Temporal Behaviour ◽  
System Designer ◽  
Functional Aspects ◽  
Time Systems

Model checking is a widely used technique for the formal verification of computer systems. However, the suitability of model checking strongly depends on the capacity of the system designer to specify a model that captures the real behaviour of the system under verification. For the case of real-time systems, this means being able to realistically specify not only the functional aspects, but also the temporal behaviour of the system. This chapter is dedicated to modeling clocks in distributed embedded systems using the timed automata formalism. The different types of computer clocks that may be used in a distributed embedded system and their effects on the temporal behaviour of the system are introduced, together with a systematic presentation of how the behaviour of each kind of clock can be modeled. The modeling is particularized for the UPPAAL model checker, although it can be easily adapted to other model checkers based on the theory of timed automata.

scholarly journals Linear Parametric Model Checking of Timed Automata

2001 ◽  
Vol 8 (5) ◽  
Author(s):  
Thomas S. Hune ◽  
Judi Romijn ◽  
Mariëlle Stoelinga ◽  
Frits W. Vaandrager
Keyword(s):  
Model Checking ◽  
State Space ◽  
Timed Automata ◽  
Parametric Model ◽  
Model Checker ◽  
Linear Parameter ◽  
Emptiness Problem ◽  
Full Class ◽  
Parameter Constraints ◽  
Published Paper

<p>We present an extension of the model checker Uppaal capable<br /> of synthesizing linear parameter constraints for the correctness of<br />parametric timed automata. The symbolic representation of the (parametric)<br /> state-space is shown to be correct. A second contribution of this<br />paper is the identification of a subclass of parametric timed automata<br />(L/U automata), for which the emptiness problem is decidable, contrary<br />to the full class where it is know to be undecidable. Also we present a<br />number of lemmas enabling the verification effort to be reduced for L/U<br />automata in some cases. We illustrate our approach by deriving linear<br />parameter constraints for a number of well-known case studies from the<br />literature (exhibiting a flaw in a published paper).</p>

scholarly journals IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability

2021 ◽  
pp. 552-565
Author(s):  
Étienne André
Keyword(s):  
Model Checking ◽  
Real Time ◽  
Timed Automata ◽  
Robustness Analysis ◽  
Parametric Model ◽  
Timing Constraints ◽  
Real Time Systems ◽  
Model Checker ◽  
Time Systems ◽  
Timed Model Checking

AbstractReal-time systems are notoriously hard to verify due to nondeterminism, concurrency and timing constraints. When timing constants are uncertain (in early the design phase, or due to slight variations of the timing bounds), timed model checking techniques may not be satisfactory. In contrast, parametric timed model checking synthesizes timing values ensuring correctness. takes as input an extension of parametric timed automata (PTAs), a powerful formalism to formally verify critical real-time systems. extends PTAs with multi-rate clocks, global rational-valued variables and a set of additional useful features. We describe here the new features and algorithms offered by  3, that moved along the years from a simple prototype dedicated to robustness analysis to a standalone parametric model checker for timed systems.

CTL Model Checking of Web Services Composition based on Open Workflow Nets Modeling

2016 ◽  
Vol 7 (1) ◽  
pp. 27-42 ◽  
Author(s):  
Zohra Sbaï ◽  
Rawand Guerfel
Keyword(s):  
Model Checking ◽  
Web Services ◽  
Petri Nets ◽  
Business Processes ◽  
Graphical Representation ◽  
Added Value ◽  
Model Checker ◽  
Web Services Composition ◽  
Services Composition ◽  
Bpel Processes

Web services composition (WSC) has an enormous potential for the organizations in the B2B area. In fact, different services collaborate through the exchange of messages to implement complex business processes. BPEL is one of the most used languages to develop such cooperation. However, it has been proved that its use is complex and can require some expertise in XML syntax. Even its graphical representation is not evident to handle. This is why the authors propose to model Web services using oWF-nets, a subclass of Petri nets, and then, to translate them to BPEL. Whilst, a WSC is with added value only if the involved services are compatible. So in this context, across the translation proposed the researchers develop a verification layer of the WSC compatibility. Hence, they propose a framework named D&A4WSC which allows to model the WSC by oWF-nets, to check their compatibility with the model checker NuSMV and to translate them if they are compatible in BPEL processes using the oWFN2BPEL compiler. D&A4WSC permits, furthermore, to formally analyze a BPEL process.

scholarly journals Pemodelan dan Verifikasi Formal Protokol EE-OLSR dengan UPPAAL CORA

2016 ◽  
Vol 10 (1) ◽  
pp. 93
Author(s):  
Rachmat Wahid Saleh Insani ◽  
Reza Pulungan
Keyword(s):  
Model Checking ◽  
Energy Efficient ◽  
Timed Automata ◽  
Packet Transmission ◽  
Model Checker ◽  
Link State ◽  
Internet Users ◽  
Information And Communication ◽  
Fully Automatic ◽  
Verification Process

Information and Communication Technology systems is a most important part of society.  These systems are becoming more and more complex and are massively encroaching on daily life via the Internet and all kinds of embedded systems. Communication protocols are one of the ICT systems used by Internet users. OLSR protocol is a wireless network communication protocol with proactive, and based on link-state algorithm. EE-OLSR protocol is a variant of OLSR that is able to prolong the network lifetime without losses of performance.Protocol verification process generally be done by simulation and testing. However, these processes unable to verify there are no subtle error or design flaw in protocol. Model Checking is an algorithmic method runs in fully automatic to verify a system. UPPAAL is a model checker tool to model, verify, and simulate a system in Timed Automata.UPPAAL CORA is model checker tool to verify EE-OLSR protocol modelled in Linearly Priced Timed Automata, if the protocol satisfy the energy efficient property formulated by formal specification language in Weighted Computation Tree Logic syntax. Model Checking Technique to verify the protocols results in the protocol is satisfy the energy efficient property only when the packet transmission traffic happens.

Applying Formal Methods to Verify Web Services Orchestration and Choreography

2018 ◽  
pp. 221-243
Author(s):  
Zohra Sbai
Keyword(s):  
Model Checking ◽  
Web Services ◽  
Special Class ◽  
Added Value ◽  
Model Checker ◽  
Web Services Composition ◽  
Services Composition ◽  
Formal Framework ◽  
Services Orchestration ◽  
The Web

The contribution presented in this chapter is to provide a formal framework ensuring the model checking based verification of the Composition of Web Services (WSC). For this, the authors propose first to model the web services composition by an interaction of open workflow nets: a special class of Petri nets. Then, they detail how to check behavioral properties specified in temporal logic using the model checker NuSMV. A WSC is with added value only if the involved services are compatible. So, in this context, across the translation proposed, the authors develop a verification layer of the WSC compatibility. This work is developed in a framework named D&A4WSC which allows to model the WSC by oWF-nets and to check their compatibility by invoking the model checker NuSMV. Furthermore, the authors extended D&A4WSC so that it permits a web services choreography described in a WS-CDL specification. For this they developed a translation from WS-CDL to a composition of oWF-nets, so that one can verify this choreography by the aforementioned approach.

Sign in / Sign up

Export Citation Format

Share Document