1,721,043 research outputs found
FME 2003: Formal methods
No full textThis volume contains the proceedings of FM 2003, the 12th international formal Methods Europesymposium which was held in Pisa, Italy, on September 8-14, 2003
Formal Methods for Service Composition
No full textCurrent approaches to service composition
range from industrial standards (like BPEL and OWL-S)
to formal methods (like Petri nets and process algebras).
In this paper, we survey a number of such approaches
and compare them with respect to a carefully selected
set of characteristics (like exception handling and quality
of services). We conclude that formal methods, often
including tool support, are ideal to assist designers and
developers because their use leads to increased confidence
in the obtained compositions
A Model Checking Approach for Verifying COWS Specifications
Full text linkWe introduce a logical verification framework for checking functional properties of service-oriented applications formally specified using the service specification language COWS. The properties are described by means of SocL, a logic specifically designed to capture peculiar aspects of services. Service behaviours are abstracted in terms of Doubly Labelled Transition Systems, which are used as the interpretation domain for SocL formulae. We also illustrate the SocL model checker at work on a bank service scenario specified in COWS
Formal Verification of Safety Requirements on Complex Systems
No full textIn this paper we present a logical characterization, by means of ACTL formulae, of safety requirements to be formally verified over safety critical complex systems. In this class of systems the formal verification of requirements is often hardened by state explosion problems. To deal with this problem, the characterization we propose allows the satisfiability of a safety requirement over a complex system to be derived by its satisfiability over those component subsystems that are directly involved in the given requirement. The proposed methodology has been successfully used for the formal verification of safety requirements of a particular system, that is a railway computer based signalling control system
An experience in using a tool for evaluating a large set of natural language requirements
No full textRequirements analysis is an important phase in a software project. It is often performed in an informal way by specialists who review documents looking for ambiguities, technical inconsistencies and incompleteness. Automatic evaluation of Natural Language (NL) requirements documents has been proposed as a means to improve the quality of the system under development. We show how the tool QuARS Express, introduced in a quality analysis process, is able to manage complex and structured requirement documents containing metadata, and to produce an analysis report rich of categorized information that points out linguistic defects and indications about the writing style of NL requirements. In this paper we report our experience using this tool in the automatic analysis of a large collection of natural language requirements, produced inside the MODCONTROL project
Modeling Variability, Evolvability, and Adaptability in Service Computing (a vision for future research)
No full textDetecting Policy Conflicts by Model Checking UML State Machines
No full textPolicies are convenient means to modify system behaviour at run-time.
Nowadays, policies are created in great numbers by different actors, ranging from
system administrators to lay-users. However, this situation may lead naturally to
inconsistencies, a problem that has been recognized and termed policy conflict.
The adoption of a widely-used notation, with good tool support, to express the
policies, can not only support the detection, but also help all the involved actors
in understanding and resolving the conflicts. In this respect, a natural candidate
is UML due to its current wide use in the industrial practice. In this paper we
show how to model check policies expressed in UML to verify whether they are
free of conflicts: we define a correspondence between APPEL policies and UML
state machines and use UMC as a model checker. We validate the approach with
examples taken from the literature
An experience in using a tool for evaluating a large set of natural language requirements
Full text linkRequirements analysis is an important phase in a software project. It is often performed in an informal way by specialists who review documents looking for ambiguities, technical inconsistencies and incompleteness. Automatic evaluation of Natural Language (NL) requirements documents has been proposed as a means to improve the quality of the system under development. We show how the tool QuARS Express, introduced in a quality analysis process, is able to manage complex and structured requirement documents containing metadata, and to produce an analysis report rich of categorized information that points out linguistic defects and indications about the writing style of NL requirements. In this paper we report our experience using this tool in the automatic analysis of a large collection of natural language requirements, produced inside the MODCONTROL project
- …
