1,721,050 research outputs found
A Refinement Calculus for Tuple Spaces
No full textAbstractIt is fairly accepted that the realization of complex systems must be accomplished step by step from the initial specification, through a sequence of intermediate phases, to the final program. These development steps, linking a preliminary version, or description, of the program to a more detailed one, are usually called refinement steps, while the intermediate stages of a refinement process are called levels of abstraction.A refinement calculus is a means to support this modus operandi in program development, allowing linking different levels of abstraction; it introduces a precise relation between intermediate descriptions, and the rules to check whether the relation is satisfied.Tuple space languages are concurrent languages, that foster the definition of autonomous entities of computation (the processes), and offer mechanisms for their synchronization and communication. In particular, they represent one of the most acknowledged models of coordination. Tuple space languages are based on the idea that a dynamic collection of tuples can act as shared state of concurrent processes, and play the role of coordination media among them.To build a refinement calculus for tuple spaces, we address three points, in this paper: 1.(1) We single out a specification language, a variation of first-order temporal logic. Temporal relations between propositional formulae are not expressive enough to describe relations between tuple spaces, which are multisets of atoms. The specification language, called Oikostl, includes three new temporal operators that enhance the expressive power of the logic, permitting to directly link state transitions and state configurations. The semantics of the specification language is formally defined, and a set of useful properties for refinement are shown.2.(2) We introduce a reference language for tuple spaces, dubbed TuSpReL, and define its axiomatic and operational semantics. We need the former to derive properties, the latter to describe the allowed computations of a system. We relate these descriptions, and guarantee that using the axiomatic semantics we can derive properties, which are correct and complete with respect to the operational behavior. The non-deterministic features of tuple space languages make this result new, and more complex than in other programming paradigms. One of the contributions of our work is the idea to derive weakest preconditions exploiting the demonic strict choice in non-deterministic selection. The transition system defining the operational semantics is based on the new notion of enabling precondition, which exploits the angelic strict choice.3.(3) To build the refinement calculus, we take a compositional approach. We first consider the basic statements of the language, and say under which conditions they satisfy a property, then compose these proofs to derive that a system refines a specification. Finally, in the refinement calculus definition, we extend to tuple space languages the ability to exploit logic formulae to specify the behavior of unrefined modules: in the intermediate steps, a system is only partially written in the programming language, and the still unrefined features are described by logical formulae
Distributed States Logic
No full textWe introduce a temporal logic to reason on global applications.
First, we define a modal logic for localities that embeds the local
theories of each component into a theory of the distributed states of the
system. We provide the logic with a sound and complete axiomatization.
Then, we extend the logic with temporal operators. The contribution is
that it is possible to reason about properties that involve several
components, even in the absence of a global clock, as required in an
asynchronous setting. We support our proposal by working out an example, a
simple secure communication system
A Lightweight Approach to the Early Detection and Resolution of Feature Interactions
No full textThe feature interaction problem has been recognized as a general problem of software engineering, whenever one wants to reap the advantages of incremental development. In this context, a feature is a unit of change to be integrated in a new version of the system under development, and the problem is that new features may interact with the others in unexpected ways. We introduce a common abstract model, to be built during early requirement analysis in a feature oriented development. The model is common, since all the features share it, and is an abstraction of the behavioural model retaining only what is needed to characterize each feature with respect to their possible interactions. The basic constituents are the abstract resources that the features access in their operations, the access mode (read or write), and the reason of each access. Given the model, the interactions between the features are automatically detected, and the goal oriented characterization of the features provides the developers with valuable suggestions on how to qualify them as synergies or conflicts (good and bad interactions), and on how to resolve conflicts. We provide evidence of the feasibility of the approach with an extended example from the Smart Home domain. The main contribution is a lightweight state-based technique to support the developers in the early detection and resolution of the conflicts between features
Barbed Model--Driven Software Development: A case study
No full textAbstractWhen thinking of MDE, the immediate understanding is that models drive software development, in the sense that the software is constructed by transforming models from higher levels of abstraction to the point where we reach a model which is executable with the desired degree of quality characteristics. What tends to be less evident, is that, precisely in order to reach the desired quality, many other models are used in the verification and assessment of the solutions under consideration at the various stages of development. That is, looking at the development process, besides a spine of model transformations moving from highly abstract, domain related models down to concrete platform related models (programs), we can see a number of barbs, relating models in the spine to specialized models that permit specific analysis of parts of the software.In this paper we report on some preliminary work on understanding Barbed Model–Driven Software Development. We are taking an experimental attitude, designing and implementing a barb, using specific technologies and verification tools. The goal is twofold: to get acquainted with the technologies, and to provide a first assessment of their suitability for subsequent explorations. In the experiment experiment the barb deals with the verification of properties of a SOA system modelled in UML
Software specification and design: from formal methods to standard middleware
No full textSoftware Specification and Design: From Formal Methods to Standard Middleware
Detection and Resolution of Feature Interactions, the Early Light Way
No full textThe feature interaction problem has been recognized as a general problem of software engineering, whenever one wants to reap the advantages of incremental development. In this context, a feature is a unit of change to be integrated in a new version of the system under development, and the problem is that new features may interact with others in unexpected ways. We introduce a common abstract model, to be built during early requirement analysis in a feature oriented development. The model is common, since all the features share it, and is an abstraction of the behavioural model retaining only what is needed to characterize the features with respect to their possible interactions. The basic constituents are the abstract resources that the features access in their operations, the access mode (read or write), and the reason of each access. Given the model, the interactions between the features are automatically detected, and the goal oriented characterization of the features provides the developers with valuable suggestions on how to qualify them as synergies or conflicts (good and bad interactions), and on how to resolve conflicts. We provide evidence of the feasibility of the approach with an extended example from the Smart Home domain. The main contribution is a lightweight state-based technique to support the developers in the early detection and resolution of the conflicts between features
Applying Refinement Calculi to Software Process Modelling
No full textA refinement calculus provides a number of advantages to
program development, besides correctness, like clarification
of the goals of the program and effective documentation of
the design choices. In this paper, we provide evidence that
the same advantages can be obtained also in the case of those
special programs that are known as enactable process models.
The evidence is put forward by means of an example, a small
Concurrent Engineering problem inspired to the IWSP7 problem.
We assume that the enactment is done by rules in tuple spaces,
and use a refinement calculus based on a temporal logic that
builds on that of Unity. Finally, we show how the approach
leads to seamless integration with existing process engines
(the Oikos one in our case)
- …
