Feature Integration in Requirements Engineering
ESPRIT Working Group 23531
ESPRIT Working Group 23531
In this paper, we focus on a refinement method for an object oriented algebraic formalism, called ETOILE-specifications. Étoile-specifications extend algebraic specification techniques to deal with concurrent (active) object systems. The dynamic behavior of object systems rely on implicit states used as modifiers of semantics of functionalities (or methods). Although most people affirm that objects preserve the ``good properties'' of modularity, we show that the global correctness of a system cannot be established from the local correctness of each object. This is due to the concurrency between objects. To circumvent this non modular behavior of objects, we propose a refinement theory (abstract implementation) which allows to retrieve incrementality to establish correctness. We prove that usual results concerning reuse of implementations are extended to ETOILE-specifications.
In dynamic testing, a program is flagged incorrect if it fails for a test set. But how far can a successful program be considered as correct? We give a definition of program correctness with respect to a specification which is adequate to dynamic testing. Similarly to the field of abstract implementation, in order to declare a program as correct, it suffices that its behavior fulfills the specification requirements. An intermediate semantic level between the program and the specification, the oracle framework, is introduced in order to interpret observable results of dynamic experiments on the program. This allows to give algebraic semantics to the program. Program correctness is then defined by some adequacy criterion between the specification semantics and the program semantics. For some specifications, there exist exhaustive test sets (the success of which means program correctness), for some other specifications, there only exist ``complete'' (but not exhaustive) test sets.
We introduce a notion of time into the algebraic specification framework, on the one hand for dealing with classical temporal constraints, and on the other hand to specify functions whose semantics is timely dependent. Syntax, semantics and inference system for real-time algebraic specifications are defined. A small example is also developed in order to help intuition.
We introduce a notion of time into the algebraic specification framework, on the one hand for dealing with classical temporal constraints, and on the other hand to specify functions whose semantics is timely dependent. Syntax, semantics and inference system for real-time algebraic specifications are defined. A small example is also developed in order to help intuition.
One of the novel features of CASL, the Common Algebraic Specification Language, is the provision of so-called architectural specifications for describing the modular structure of software systems. A discussion of refinement of CASL specifications provides the setting for a presentation of the rationale behind architectural specifications. This is followed by details of the features provided in CASL for architectural specifications, hints concerning their semantics, and simple results justifying their usefulness in the development process.
Requirements engineering specifications can greatly benefit from formal methods when concerned with justifying the correctness of specifications and proofs. Albert II is a formal specification language for capturing functional requirements inherent to real-time, distributed systems. Targeted to requirements engineering activities, Albert II exhibits a high expressiveness through a large range of constructs. Their interactions being however very intricate, these constructs may hamper the reasoning capabilities. Formal reasoning is nevertheless still possible because the language is grounded on a real-time core logic. We motivate our approach to the construction of a formal verification system for this core logic.
Albert is a specification language intended to support the eliciting of functional requirements proper to composite and distributed real-time systems. To achieve mathematical rigour Albert has been endowed with a formal semantics. Compositionality is one of our primary target. The models of the atomic components are first individually built and then composed to yield the semantic model of the full specification. We define an intermediate language, Albert-kernel, retaining all the important concepts of Albert. With this language the main concepts of Albert (agent decomposition, action, information and perception) have a direct correspondence. We provide formal semantics for Albert-kernel. An axiomatisation of the semantics in terms of set theory and timed state sequence structures could be used as a basis for semantic reasoning tools since they usually use a less expressive logic into which our formalism could be readily abstracted.
.
The PEPA language is supported by a suite of modelling tools which assist in the solution and analysis of PEPA models. The design and development of these tools have been influenced by a variety of factors, including the wishes of other users of the tools to use the language for purposes which were not anticipated by the tool designers. In consequence, the suite of PEPA tools has adapted to attempt to serve the needs of these users while continuing to support the language designers themselves. In this paper we report on our experiences with the PEPA tools and give some advice gained from our experiences.
We present two logics that allow specifying distributed information systems, emphasizing communication among sites. The low-level logic D0 offers features that are easy to implement but awkward to use for specification, while the high-level logic D1 offers convenient specification features that are not easy to implement. We show that D1 specifications may be automatically translated to D0 in a sound and complete way. In order to prove soundness and completeness, we define our translation as a simple map of institutions. Our result may be useful for making implementation platforms like CORBA easier accessible by providing high-level planning and specification methods for communication.
We propose a framework for ``probabilistic functional testing.'' The success of a test data set generated according to our method guarantees a certain level of confidence into the correctness of the system under test, as a function of two parameters. One is an estimate of the reliability, and the other is an estimate of the risk that the vendor takes when (s)he notifies this reliability percentage to the client. These results are based on the theory of ``formula testing'' developed in the article. We also present a first prototype of a tool which assists test case generation according to this theory. Lastly, we illustrate our method on a small formal specification.
We consider the feature interaction problem in the context of the use of the PEPA stochastic process algebra.
Performance Evaluation Process Algebra (PEPA) is a formal language for performance modelling based on process algebra. It has previously been shown that using the process algebra apparatus compact performance models can be derived which retain the essential behavioural characteristics of the modelled system. However no efficient algorithm for this derivation was given. In this paper we present an efficient algorithm which recognises and takes advantage of symmetries within the model and avoids unnecessary computation. The algorithm is illustrated by a multiprocessor example. Although it is much more efficient than the previously proposed techniques the algorithm is subject to some limitations. In particular it will not always achieve the best possible aggregation. This case is also illustrated by an example, and we discuss when this limitation is likely to have an impact on performance analysis.
A specification formalism for real-time systems defines a class of timed omega -languages, whose letters have real-numbered time stamps. Two popular ways of specifying timing constraints rely on the use of clocks, and on the use of time bounds for temporal operators. However, temporal logics with clocks or time bounds have undecidable satisfiability problems, and finite automata with clocks (so-called timed automata) are not closed under complement. Therefore, two fully decidable restrictions of these formalisms have been proposed. In the first case, clocks are restricted to event clocks, which measure distances to immediately preceding or succeeding events only. In the second case, time bounds are restricted to nonsingular intervals, which cannot specify the exact punctuality of events. We show that the resulting classes of timed omega -languages are robust, and we explain their relationship.
A new treatment of data refinement in typed lambda calculus is proposed, phrased in terms of pre-logical relations [HS99] rather than logical relations, and incorporating a constructive element. Constructive data refinement is shown to have desirable properties, and a substantial example of refinement is presented.
We reflect on our experiences from work on the design and semantic underpinnings of Extended ML, a specification language which supports the specification and formal development of Standard ML programs. Our aim is to isolate problems and issues that are intrinsic to the general enterprise of designing a specification language for use with a given programming language. Consequently the lessons learned go far beyond our original aim of designing a specification language for ML.
Due to practical limitations in software and hardware, data type implementations are always bounded. Such limitations are a frequent source of faults which are difficult to find out. As soon as boundaries are clearly identified in a specification, functional testing should be able to address any boundary fault. We propose to enrich a data type specification formalism, namely algebraic specifications, allowing a natural description of data type boundaries. This enhancement allows us to adapt the existing testing theory, the method and the tool, initially dedicated to functional testing from unbounded data type specifications. Several examples of test data selection with the LOFT tool, from two bounded data type specifications will illustrate the benefit of our approach: an assisted test selection process, formally defined in a functional testing theory, allowing adequate coverage of both data types bounds and the definition domains of the specified operations.
We propose a feature construct for defining features, and use it to provide a plug-and-play framework for exploring feature interactions. Our approach to the feature interaction problem has the following characteristics: (a) features are treated as first-class objects during the development phase; (b) a method for integrating a feature into a system description is described. It allows features to override existing behaviour of the system being developed; (c) a prototype tool has been developed for performing the integration; (d) our approach allows interactions between features to be witnessed. In principle, our approach is quite general and need not be tied to any particular system description language. In this paper, however, we develop the approach in the context of the SMV model checking system. We describe two case studies in detail: the lift system, and the telephone system.
A feature is an increment of functionality that can be added to an existing system. Many features override the default behaviour of the system, and can lead to unexpected situations. Adding several features to a system is very likely to introduce inconsistencies among their functionality, even if each feature works correctly in isolation. To facilitate the development of features and the detection of inconsistencies between features, using model checking, we extend Promela with a Feature Construct. This construct allows us to define changes to a given Promela program in a clearly structured and intuitive way. The features thus defined are then automatically integrated into the Promela description of the base system by means of a preprocessor. The developer need not (and should not) alter the original code except through the feature integration process.
Feature-oriented specification addresses the problem of how to add new functionality to a system in a systematic way. A feature is a unit of functionality that can be added to an existing system. Sometimes however, combinations of features produce unexpected results. This phenomenon has become known as feature interaction. Features and feature interactions can be found in any system that is enhanced with new or optional functionality. Feature-oriented specification addresses three central questions: begin itemize item how to specify features for a system, item how to add features to the system, and item how to detect interactions among features. end itemize The method proposed here is to extend specification languages with constructs for defining features, so-called feature constructs. Each feature construct is complemented by a notion of feature integration: a method for adding a feature definition to the specification of a system. Feature integration gives semantics to a feature construct. This thesis details feature constructs for three specification languages, SMV , Promela and CSP , and demonstrates their use in examples and case studies. For SMV and CSP , formal semantics of the feature constructs are developed, too. All three languages investigated are model checking languages, and we investigate the use of model checking to detect feature interactions.
In this paper we study two possible semantics for the real-time logic MTL (Metric Temporal Logic). In the first semantics, called dense time semantics, time is modeled by the positive real numbers. In the second one, called fictitious clock semantics, real-time information is delivered by a global fictitious clock. We show that the fictitious clock semantics can be viewed as an abstraction of the dense time semantics. This abstraction relation is formalized by a parametric conservative connection. This formalization can be used to partially decide undecidable problems in the dense time semantics by reasoning on the fictitious clock semantics.
In this paper we define a real-time logic called SC logic. This logic is defined in the framework of State Clock automata, the state variant of the Event Clock automata of Alur et al. Unlike timed automata, they are complementable and thus language inclusion becomes decidable. SC automata and SC logic are less expressive than timed automata and MITL but seem expressive enough in practice. A procedure to translate each SC formula into a SC automaton is presented. The main contribution of this paper is to complete the framework of this class of determinizable automata with a temporal logic and to introduce the notion of event clock in the domain of temporal logic.
This paper presents a complete axiomatization of fully decidable propositional real-time linear temporal logics with past: the Event Clock Logic ( ECL ) and the Metric Interval Temporal Logic with past ( MITL ). The completeness proof consists of an effective proof building procedure for ECL . From this result we obtain a complete axiomatization of MITL by providing axioms that allows the translation of MITL formulae into ECL formulae, the two logics being equally expressive. Our proof is structured to yield a similar axiomatization and procedure for interesting fragments of this logic: the linear temporal logic of the real numbers ( LTR ), the fragment with only past clocks.
This paper summarises and systematizes the link between Counterfactual and Updates.
Various formalizations of the concept of ``refinement step'' as used in the formal development of programs from algebraic specifications are presented and compared.
The Common Framework Initiative (CoFI) is an open international collaboration which aims to provide a common framework for algebraic specification and development of software. The central element of the Common Framework is a specification language called CASL for formal specification of functional requirements and modular software design which subsumes many previous algebraic specification languages. This paper is a brief summary of past and present work on CoFI.
In [Andreka], a large number of completeness results about variants of discrete linear-time temporal logic are obtained. One of them is left as an open problem: the completeness of the logic of initially and next, for which a deductive system is proposed. This simple logic is of practical importance, since the proof of program invariants only require these modalities. We show here that the conjectured completeness of this system indeed holds; further, we show that the corresponding decision problem is NP-complete.
Traditional information system specifications are fixed: the rules of the system are frozen at specification time. In practice, most systems have to change their rules in unexpected ways during their lifetime: business rules evolve with market pressures, the legal constraints are modified. We present here a simplified and more classical variant of a temporal logic that deals with specification evolution. It is a linear time temporal logic with two levels of time: intervals, interrupted by mutations (changes of rules), which compose lifes of the system.
The advantages of using stochastic process algebra to specify performance models are well-documented. There remains, however, a reluctance in some quarters to use process algebras; this is particularly the case amongst queueing theorists. This paper demonstrates the use of a Markovian process algebra to represent a wide range of queueing models. Moreover, it shows that the most common interactive behaviours found in queueing systems can be modelled simply in a Markovian process algebra, and discusses how such specifications can lead to an automated numerical solution method. An additional objective of this work is to specify queueing models in a form which facilitates efficient solution techniques. It is intended that characterising the syntactic forms within the Markovian process algebra which give rise to these efficient solution methods will subsequently allow the methods to be applied to a much wider range of models specified in the process algebra.
Stochastic process algebras have become an accepted part of performance modelling over recent years. Because of the advantages of compositionality and flexibility they are increasingly being used to model larger and more complex systems. Therefore tools which support the evaluation of models expressed using stochastic process algebra must be able to utilise the full range of decomposition and solution techniques available. In this paper we study a class of models which do not give rise to a product form solution but can nevertheless be decomposed into their components without loss of generality. We also exemplify the use of the Markovian process algebra PEPA with the spectral expansion technique which enables a class of PEPA models with infinite state space to be solved numerically.