Related Experiment Videos
A verification strategy for web services composition using enhanced stacked automata model
Danapaquiame Nagamouttou1, Ilavarasan Egambaram1, Muthumanickam Krishnan1
1Department of Computer Science and Engineering, Pondicherry Engineering College, Pondicherry, 605014 India.
Springerplus
|March 27, 2015
Summary
This study introduces an Enhanced Stacked Automata Model (ESAM) for verifying composed web services, improving detection of dead transitions and deadlocks in non-deterministic systems.
Area of Science:
- Computer Science
- Software Engineering
Background:
- Service-Oriented Architecture (SOA) is prevalent in enterprise applications, with web services enabling composition of business processes.
- Business Process Execution Language (BPEL) is a standard for defining web service compositions, but verification of these compositions remains a challenge.
- Existing verification models for web services often lack support for non-deterministic systems and key properties like deadlocks and dead transitions.
Purpose of the Study:
- To propose a novel model, the Enhanced Stacked Automata Model (ESAM), for verifying composed web services.
- To address limitations in existing models by incorporating verification of properties such as dead transition, deadlock, reachability, safetyness, and liveness for non-deterministic systems.
- To demonstrate the effectiveness of the proposed model in identifying critical verification issues.
Main Methods:
- Web services were composed using Business Process Execution Language for Web Service (BPEL4WS).
- The composed services were converted into the Enhanced Stacked Automata Model (ESAM), integrating Muller Automata (MA) and Push Down Automata (PDA).
- The ESAM model was translated into Promela language for verification using the Simple Promela Interpreter (SPIN) tool.
Main Results:
- The proposed ESAM model successfully evaluated correctness properties for non-deterministic systems.
- Verification using the SPIN tool demonstrated superior performance in detecting dead transitions and deadlocks compared to existing models.
- The study confirmed the model's capability to identify critical issues in web service compositions.
Conclusions:
- The Enhanced Stacked Automata Model (ESAM) provides an effective approach for verifying complex, non-deterministic web service compositions.
- The ESAM model enhances the reliability of enterprise applications built on Service-Oriented Architecture.
- This work contributes a significant advancement in the formal verification of web services, addressing previously unmet needs.
Related Concept Videos
02:16Stereotype Content Model
15.7K
The Stereotype Content Model (SCM) was first proposed by Susan Fiske and her colleagues (Fiske, Cuddy, Glick & Xu, 2002; see also Fiske, 2012 and Fiske, 2017). The SCM specifies that when someone encounters a new group, they will stereotype them based on two metrics: warmth—or that group’s perceived intent, and how likely they are to provide help or inflict harm—and competence—or their ability to carry out that objective. Depending on the warmth-competence...
15.7K
01:17Strategies of Self-Presentation II: Self-Verification
267
Self-verification is a fundamental psychological drive wherein individuals seek affirmation of their self-concept from others, striving for consistency between their internal self-view and external perceptions. This drive operates even when the self-concept is negative, influencing interpersonal behavior and feedback preferences in complex and often counterintuitive ways. Unlike the self-enhancement motive, which seeks positive evaluations, self-verification prioritizes coherence and...
267
01:30Simplified Synchronous Machine Model
926
The Synchronous Machine Model is a fundamental tool in analyzing and ensuring the transient stability of power systems. This model simplifies the representation of a synchronous machine under balanced three-phase positive-sequence conditions, assuming constant excitation and ignoring losses and saturation. The model is pivotal for understanding the behavior of synchronous generators connected to a power grid, particularly during transient events.
In this model, each generator is connected to a...
In this model, each generator is connected to a...
926
01:21Mechanistic Models: Overview of Compartment Models
543
Mechanistic models, a category encompassing both physiological and compartmental modeling, differ from empirical models' approaches to incorporating known factors about the systems being modeled. Empirical models describe data with minimal assumptions, while mechanistic models aim to provide a robust description of available data by specifying assumptions and integrating known factors about the system. Compartmental analysis is a key example of a mechanistic model in pharmacokinetics and...
543
01:34Woodward–Hoffmann Selection Rules and Microscopic Reversibility
4.2K
Electrocyclic reactions, cycloadditions, and sigmatropic rearrangements are concerted pericyclic reactions that proceed via a cyclic transition state. These reactions are stereospecific and regioselective. The stereochemistry of the products depends on the symmetry characteristics of the interacting orbitals and the reaction conditions. Accordingly, pericyclic reactions are classified as either symmetry-allowed or symmetry-forbidden. Woodward and Hoffmann presented the selection criteria for...
4.2K
01:26Constraints and Statical Determinacy
1.1K
In structural engineering, the equilibrium of a system is not only determined by its equations of equilibrium but also with the help of constraints. Constraints refer to restrictions on the motion of a system. The proper combinations of constraints can minimize the total number of constraints needed to maintain a system in mechanical equilibrium. When this happens, the system is said to be statically determinate. For such systems, the unknown reaction supports can be estimated using equilibrium...
1.1K