Download this document as dvi file or as gzipped PostScript.

Feature Integration in Requirements Engineering

Working Group 23531

Technical Report for Year 3

March 2001

Coordinator:
Mark Ryan
School of Computer Science
University of Birmingham
Birmingham B15 2TT, UK.
Tel: +44 121 414 7361. Fax: +44 121 414 4281.
http://www.cs.bham.ac.uk/~mdr/,
Email: M.D.Ryan@cs.bham.ac.uk

Introduction

FIREworks is a Working Group that addresses the problem of adding features to complex software products, in particular software for telecommunication services. It aims to provide a feature-oriented approach to software design including requirements specification languages and verification logics, as well as a method for their usage. FIREworks began on 1 May 1997; this document is its third year report. The third year would have spanned 1 May 1999 to 30 April 2000, but we were fortunate in being granted an extension until 30 November 2000. This final year therefore covers the period 1 May 1999 to 30 November 2000.

The first year's report describes the importance and industrial relevance of FIREworks, as well as giving the full list of members and subgroups. All this information is available from the FIREworks home page

http://www.cs.bham.ac.uk/ mdr/fireworks/

During the final year, we added two further participants to our Working Group:

1.: Laboratoire Logiciels, Systemes, Reseaux (LSR) Institut d'informatique et de mathematiques appliquees de Grenoble (IMAG), BP 72, 38402 St Martin d'Heres, France. Site leader: Farid Ouabdesselam
Other members: Lydie du Bousquet, Jean-Luc Richier, Nicolas Zuanon
2.: LORIA, Universite Henri Poincare, BP 239, 54506 Vandoeuvre, France. Site leader: Jeanine Souquieres
Other members: Dominique Mery

Summary and main conclusions

Like the first and second years, the third and final year of FIREworks has been a substantial success. Three substantial events have taken place during that year:

MOVEP Summer School with FIREworks participation, Nantes, France, 19-23 June 2000.
FIREworks Workshop 3, held in Glasgow, UK,15-16 May 2000, with the title: Workshop on Language Constructs for Describing Features. We had 13 contributions both internal and external to FIREworks membership;
Participation in the international Feature Interaction Workshop, also in Glasgow, UK, 17-19 May 2000, with three contributions from FIREworks members (Ryan; Mery; Bouma).

Many papers have been published or are currently in progress (see References). Joint authorship across sites gives evidence of co-operation between members. Other highlights of the year include:

Proceedings of FIREworks WS3 published by Springer-Verlag [GR01];
Participation of two new partner sites active in feature interaction;
International Feature Interaction Workshop Contest won by FIREworks team.

Research in the Third Period

AALB: Aalborg, Denmark

During the final project year we have been working on two activities: (1) We have continued the work initiated in the second year on protocol modelling, and (2) We have collaborated with partners within Fireworks on stopwatches of timed automatons.

Protocol modelling using abstractions.

We showed in an earlier paper how to model parts of a real-life protocol for power control of a audio/video equipment. However, it was not possible to model and verify the full protocol taking all modules into account. During the final project year we have developed a proof methodolgy whereby one can verify the full system using abstraction and compositionality [JLS00]. The methodology seems very

promising in order to cope with the state-explosion problem associated with verification of complex real-time systems.

Stopwatch Automata.

For purposes of efficiency, the modelling language of the realtime verification tool UPPAAL was initially designed to be rather limited in terms of expressive power. However, a number of features have been added during the period of the Fireworks project. In particular, an extension of UPPAAL with stopwatches (clocks that may be stopped occasionally) has been given [FC00]. The expressive power of this extension is shown to be equal to the full class of linear hybrid automata thus allowing an approximate analysis of such systems to be carried out using the efficient data structures and algorithms of UPPAAL. This work is carried out in the context of the Fireworks project in collaboration with Franck Cassez, Nantes.

BHAM: Birmingham, UK

The final year of FIREworks has been our most active so far!

We were delighted that our entry to the International Feature Interaction Workshop Contest was judged to be the winning entry in the category of two-feature interactions.
We completed our work on the SMV feature construct.
We began two new pieces of work, aimed at verifying feature interactions without the cost of model checking. The idea is to study which properties are preserved by the feature construct.
Malte Plath submitted his thesis entitled Language Constructs for Defining Features for Reactive Systems [Pla00], and will be examined in March 2001.

Contest

The second Feature Interaction Contest was held in conjunction with the 6th International Workshop on Feature Interactions in Telecommunication and Software Systems (FIW'00) [CM00]. The aim of the contest was to compare various methods and tools for detecting feature interactions. To enable a comparison, the contest's objective was to detect interactions among a given set of features for a given telephone system. The contest instructions contained detailed (albeit imprecise) specifications of the base system and twelve features.

In our entry, we used a combination of two techniques: static (syntactic) analysis and model checking using the model checker FDR [Ros97]. More details can be found in our paper [PR01].

We are delighted to report that our entry won the contest in the category of two-feature interactions. For a summary of the results produced by each of the contestants, see [KMMR00].

SMV construct

We have completed a journal paper about the feature construct for SMV [PR99]. The results in those papers were entirely experimental. In order to have a good theoretical base, we developed a precise semantics for the feature construct for SMV. Using such semantics, we can explore in what circumstances the feature construct is independent of the syntax of the base program to which the feature is applied, and other properties of features. This allowed us to explore when features commute with each other, and, more generally, to explore what classes of features are `interaction-friendly' with respect to other classes. It is also a step towards being able to verify the feature itself, independently of the system to which it is added. Further details can be found in our paper [PR00]

Preserving properties by the feature construct

Together with the Namur and Nantes sites, we studied a framework in which we can prove that certain features do not destroy properties added by other ones. The result is based on the idea that a feature which adds to the capabilities of a user (and does not subtract from them) should not break properties which assert capabilities of this user.

Many features of telephone systems are designed so that they add to the capabilities (or powers), of the subscribing user, without subtracting from them. For example, a user j who subscribes to call-forwarding now has the power to forward his or her calls to another user, but has not lost any capabilities in the process. When this is the case, we say that the feature is j-conservative. More generally, if U is a set of users, a feature is U-conservative if any behaviour of the system which U could enforce before the feature was added, U can also enforce it after the feature is added. The principal idea in our paper [CRS01a] is that a U-conservative feature does not break properties which assert capabilities of the group U of users. To formalise this intuition, we propose to use Alternating-time Temporal Logic [AHK97] (ATL). For more details, see our paper [CRS01a].

Probabilistic model checking

We have continued in the following three main directions:

Efficient probabilistic verification:: We have demonstrated that using boolean variable ordering based on the Kronecker representation leads to a very compact representation of the probabilistic models in MTBDDs [dAKN⁺00]. Model checking of qualitative PCTL properties (with probability 1 or 0) can be reduced to reachability analysis, and is very efficient. Model checking of quantitative properties, however, is orders of magnitude less efficient than for sparse matrices. We are currently working on a hybrid data structure, combining MTBDDs and a full vector, to improve the performance of numerical calculations. Preliminary results are encouraging. The Probabilistic Symbolic Model Checker PRISM is nearing release. For more information see www.cs.bham.ac.uk/ dxp/prism/
Probabilistic timed automata:: We have considered the probabilistic timed automata model introduced in [KNSS99] and improved the efficiency of the corresponding model checking procedure by formulating two algorithms, one based on forward reachability [KNSS01] and anotehr based on backwards reachability. We have also derived an approximate algorithm for model checking of continuous probabilistic timed automata based on subdivisions of the region graph [KNSS00]. We are currently developing a prototype tool which accepts a discrete-probabilistic timed automaton and generates input into the PRISM tool. The PRISM tool then can calculate the probability of reaching a particular target set of states within a given time deadline.
Probabilistic hybrid automata:: We have introduced probabilistic hybrid automata and formulated model checking algorithms for subclasses of those based on translation into probabilistic timed automata. This is described in [Spr00] and PhD thesis by Jeremy Sproston entitled Model Checking for Probabilistic Timed and Hybrid Systems and defended successfully.

FUNDP: Namur, Belgium

Our research this year has mainly focused on the use of the specific advantages of the introduction of decision-theoretic notions, based on agents [PHS99], for features [CRS01b]. Our work on tools for feature-oriented specifications has been pursued. Notably, the animator has been enriched and deals with a larger specification language.

Many interesting alleys of research are still left open, however. We hope to investigate:

The extension of scenario-based development [HHJP99] to the development of features;
The extension to probabilities and real-time: although these extension are most likely to be conceptually orthogonal, they seem required in the current main domain of features, namely telephony.
We think that our agent-based modelling of enterprises [FHP00,Pet99] could also benefit from the feature concept.

LFCS: Edinburgh, UK

A feature construct for the PEPA modelling language had previously been developed at the Edinburgh site. This allowed a sequence of performance models of computer systems to be constructed and maintained in step with feature additions to the system which they described. The idea behind this was presented at the Evry meeting and a short paper on this construct was accepted for inclusion in the proceedings of the Fifteenth Annual UK Performance Engineering Workshop [GH99]. The final year of research at the Edinburgh site saw further application of the newly created feature construct for PEPA. A longer paper on the construct and its semantic foundations was presented at the Glasgow meeting of the FIREworks project [GH01]. The use of this construct was exercised with a case study of modest size.

The added expressive power afforded by the feature construct addition to the PEPA language was again extended to provide a novel higher-order modelling paradigm for stochastic process algebras [GH00].

One of the subsidiary goals of the past year of research at the Edinburgh site was to extend the PEPA support tools to deliver effective support for the use of the feature construct extensions in structured whole-lifecycle performance modelling of computer and telecommunications systems. Two developments of this were carried out [Hun99,Wan00] and other are in progress, including the integration of the PEPA Workbench with the Caesar/Aldebaran Development Package (CADP). This last implementation work should further promote the takeup of the PEPA language by industrial users: CADP is a practical software engineering toolbox for designing protocols and distributed systems.

PEPA is supported both by a logical specification method and by well-founded structured transformation and decomposition techniques. These areas of work were also addressed this year, leading to some promising techniques which will be suitable for further study [CGHR00,TH00,Hil01]. The paper on using modal logic to express performance measures is a development of earlier work extending Larsen and Skou's Probabilistic Modal Logic (PML).

IRST: Trento, Italy

SMV NuSMV

The activity of IRST in the third year was tackled the development and practical application of automatic techniques and tools for the verification and validation of specifications written in different styles, along the following lines.

SAT-based NUSMV: In the first two years, a general platform for model checking, called , was developed starting from the system developed at CMU [McM93]. is an industrial strength model checker, customizable and extensible, robust, and close to the standards required by industry [CCGR99,CCGR00]. provides for full LTL and CTL model checking, and features an interactive simulator and a graphical user interface. In the third year, was extended with Bounded Model Checking, a new symbolic model checking technique proposed in [BCCZ99b,BCCZ99a]. Given a limit on the length of the paths to be explored, Bounded Model Checking reduces an LTL verification problem to a propositional satisfiability (SAT) problem, that can then be provided to an efficient SAT solver. If a propositional model is found, then a counterexample to the model checking problem can be constructed. For certain applications domains, is shown to outperform BDD-based decision procedures. The distinguishing features of the SAT-based component of are that it relies on the use of RBC to generate compact propositional encodings [ABE00], and it is able to handle the full SMV language [CGR⁺00].
Industrial applications: Formal methods were applied in a technology transfer activity in the design, verification and validation of industrial controllers. The issues related to the integration of the formal methodology within an existing software development process [Cim01] proved to be extremely relevant. Of particular interest was the problem of detecting feature interactions for highly parameterized controllers, able to perform different functions depending on the user-requested functions. At the design level, an imperative style language was developed, and a verification engine based on NuSMV was developed. This activity is currently covered by a non-disclosure agreement. Further details will become available in publications currently under preparation.
Planning via Model Checking: In the first two years, the problem of generating plans was tackled using Symbolic Model Checking techniques. A planning problem is reformulated as a synthesis problem for finite state automata, and symbolic model checking techniques are applied for the representation and the search of the automaton representing the planning domain. In the third year, the problem of conformant planning, i.e. planning under the assumption that the state of the machine is not observabile at run-time, was tackled. In particular, the preliminary work in [CR99], based on fully symbolic techniques, was extended with the integration of explicit state model checking [CR00]. Interesting relationships were also established with the problem of generating reset sequences in hardware circuits.

IST: Lisbon, Portugal

The activities of the IST site focused on logical approaches to system specification and verification, with emphasis on concurrency and distribution, as well as on hybrid and probabilistic aspects. Special attention was recently dedicated to frameworks based on extensions of the situation calculus, observational logic and type theory. A general purpose algebraic theory of combination of logics is also being pursued, with obvious applicability within FIREworks.

The situation calculus front was pursued with [MPP⁺00,PSSM00], both also addressing probabilistic issues. This line of research is also the subject of the PhD thesis [Ram00]. Further investigations on probabilistic systems have been pursued in the submitted PhD thesis [Mat00]. Recent developments can be found in [MMN⁺00,MSS00,SM99]. Hybrid systems and logics have also been under investigation [Lou], and are the subject of the PhD thesis in preparation [LS00].

Other approaches to the study of concurrent systems are also under investigation: observational logic [Res99,Res00], and type theory [NR00,RL99,RV00a,RRV99,VR99]. The latter topic is also the subject of the PhD thesis [Rav00].

As far as combining logics is concerned, new results can be found in [CMSS00,RSSV00] and are the subject of the PhD thesis [Cal00].

LAMI: Evry, France

The research at LaMI concerning the topics of FIREworks is mainly devoted to three aspects of the feature interaction problem.

1.

Detecting interactions implies to "understand" (at least partially) the notion(s) of interaction(s). Classically, the way people understand feature interactions strongly depends on the feature conception language. For example, in [Zav98], the virtual architecture D.F.C. is used to describe systems, and interactions are expressed in the frame of this description. More precisely, in the frame of a formal approach the characterisation of the existence of an interaction strongly depends on the definition of a (feature) specification : for example in [YO98], feature specifications are described as state transition diagrams, and the different notions of feature interactions are defined on the loss or the appearance of some states and transition when combining features.

Thus, in order to give generic definitions of interactions, we give generic definitions of feature and feature system specification. To reach this purpose, we define an appropriate ``institution-like'' logic-independent framework (in [GAG00] and [GAG01] ).

Our definitions of feature interactions are based on the following claiming :

when a new feature is plugged on a system, two kinds of perturbations can occur, which can respectively be represented by two types of logical properties :

(a): Emerging properties: the feature under analysis does more services than scheduled (by its specification) when it is plugged on the system.
(b): Lost properties: The feature under analysis does less services than scheduled when it is plugged on the system.

The existence of a property of one of these types reveals a feature interaction (of course, whether this interaction is good or bad is an expert matter).

All formalisms to be used for conception need to supply mechanisms for building large specifications. We have defined the notions of enrichment, union and abstract implementation in our feature-oriented-framework. Here, enrichment can be used to build new features from an existing one by increasing its capabilities while preserving its specified behaviour. Union can be used to build new features by putting together the capabilities of existing ones.
Abstract implementation aims at defining a methodology allowing to design system by successive layers of specifications between the requirements and the final program system. Each pair of successive layers reflect certain design decisions. We have defined the notion of abstract implementation of feature and feature system. We think that this technique may help at detecting interactions as soon as possible and should allow specifier to only focus on the interactions induced by design decisions at each step of implementation.

2.

A definition of an integration method taking into account features interaction, is in progress through the French project Valiserv. This project is a partnership between two French research laboratories in computing science and two French companies:

(a): France Telecom and TNI,
(b): La.M.I of the University of Evry and LSR-IMAG of the university of Grenoble.

The aim of the method is twofold:

(a): a flexible features composition,
(b): features interaction detection based on testing techniques and expert decision.

The main underlying idea is that the way feature are composed should give some guidelines to classify both undesirable and desirable interactions. Then, some pertinent scenarios have to be selected in order to fit with the classification induced by the composition.
In this way, we have defined a framework (i.e. logic-independent) which supports these integration steps [BGK01].
This work has been presented during the last FiREworks meeting in Glasgow.

3.

In order to detect interactions, we are also investigating a static analysis of feature description given as diagrams of typical scenarios. By using classical resolution procedure, we aim at extracting divergent points between two different description. These points may be considered as original starting point of a potential interaction.

LSR: Grenoble, France

Prior to our joigning to FIREworks, we had already been involved in research addressing the problems of Feature Integration and Interaction [dBORZ98]. Since then we have primarily worked on two points: - extending our modeling technique of telecom systems in order to make it more modular, - designing of a scenario language based on the notion of behavioral patterns already successfully used) to guide the testing process of integrated features.

We have tackled the problems of feature validation and feature interaction at the specification level, in order to focus on the logical aspects of the features as well as on the identification of feature misconceptions [dBORZ00].

Most approaches dealing with the problem of feature modeling propose an integration operation which alters deeply the initial model. As a consequence, the complexity of the model resulting from an integration is higher than the added complexities of the initial model and the feature to be integrated. The operation of removing a feature from a model may as well become impracticable.

Our modeling work is original in the sense that it distinguishes the features from the basic system and defines clearly their relationships, thanks to two dedicated operations which have been well defined : composition of features and integration of features.(similar ideas can be found in one of our FIREworks partner's work (BHAM)). This modeling work is also specific because it provides a homogeneous way of handling all three specifications which compose a feature, namely the feature behaviour, the feature requirements and the feature usages. This has resulted into a unified framework to both model the features and validate them.

To reduce the complexity of the model, we have taken advantage of the synchronous approach which avoids the state explosion problem attached with the asynchronous parallel systems. The model we have come up with is also executable, a very interesting characteristic since it facilitates animation and testing.

We have investigated a set of specialised modeling patterns to provide a highly modular specification which keeps apart the basic service and the additional features: thus, each feature can be independently coded. Yet, the relation between one feature and the remaining of the system is clearly defined.

A modular specification allows both the modeling and the validation of features in an incremental manner.

The validation is performed using our automated testing tool Lutess [dBORZ99,dBZ99] which turned out to be well-adapted to this activity in general and to the interaction detection problem more specifically.

During this last year we have enriched Lutess with a testing technique based on extended behavioral patterns. Behavioral patterns are used by Lutess to guide its test data generation process, by ensuring that the most interesting input sequences are much more likely to occur. A set of behavioral patterns is associated with each feature. A language (including several operations) has been defined to combine patterns in order to test effectively each combination of features.

An additional experiment has been conducted to demonstrate the advantages of testing over model-checking, regarding the problem of feature interaction detection [dB99a].

The whole work has resulted into two successfull defended PhD theses [dB99b,Zua00] and also a set of papers and tutorials or invited conferences.

In terms of industrial involvment, we have had several meetings with our supporter France Telecom and we have been invited by Ericsson to deliver a seminar in Rome [Oua99].

MAG: Magdeburg, Germany

In this short report we describe the research activities and results of our group within the FIREworks project during the year 2000. Besides participating in both FIREworks workshops (Septemer 1999 and May 2000), head of this department, Prof. Dr. G. Saake, visited the IFAC conference (Bratislava, Slovakia) for presenting a FIREworks-related paper.

Besides that, as most of our research fits within the topic of this project - namely, the runtime manipulation and interaction of different features (as strcutural and behavioural aspects) in complex systems - we cite [ASb,TSC,ASa] for our achieved results.

NANCY: Nancy, France

Abstraction and refinement of features.

Participants: Dominique Cansell, Dominique Méry.

The composition of services and features often leads to unwanted situations, because it is a non-monotonic operation over services and features. When a new service is added to an existing system, conditions have to be checked to ensure that the resulting system satisfies a list of required properties. Following the system approach of Abrial, we develop services and features in an incremental way and use refinement to model the composition of services and features. Proof obligations state the preservation or the non-preservation of properties, namely invariant or more generally safety properties. The method helps us in understanding when a service is interfering with another, and allows us to give multiple views of each service according to the level of its refinement. Finally, we validate our method with the Atelier B tool.

A new architecture for composing features SSM.

Participants: Dominique Cansell, Dominique Méry, Dimitri Samborski.

A quick development of telecommunications and telephone services has caused a considerable complication of their managing. Service integration and marketing are slowed down or even compromised by the problem of feature interactions - a well-working service doesn't work any more once it is put together with other services in the network. It can also perturb the other services' functionalities. The present work is about the problem of feature interactions. We introduce a new architecture of the telecommunications world - SSM - that offers numerous advantages in interactions detection and managing. We propose a new specification language supported by model-checking tools for interactions detection. A resolution method is figured out whose advantage is not to change service's specification but correct the interaction on-line. A case study is done over a set of twelve services. The services are composed, their interactions are detected and mostly resolved.

NANT: IRCyN, Nantes, France

During this last year of FIREworks we have intensified the collaboration with three other FIREworks sites: Ålborg, Denmark and Birmingham, UK and Namur, Belgium.

We have worked on two main subjects:

adding features to timed automata, joint work with [AALB] Ålborg, Denmark,
studying feature interactions in the ATL logic, joint work with [BHAM] Birmingham, UK and [FUN] Namur, Belgium.

Results and publications

The main results obtained during this last year are:

the study of stopwatch automata, which are timed automata extended with a new feature: the stopwatches; we have investigated the expressive power of this model [CL00]. This work was partially achieved during a FIREworks visit in [AALB];
the study of the ATL logic to specify and verify featured system [CRS01a]. This work was achieved during two working visits in [BHAM] and in collaboration with [FUNDP].

Travel in Third Period

FIREworks Meetings

The main FIREworks event of the third period was the Third Annual Workshop which took place in Glasgow, UK in May 2000. In addition to talks from members of the group, we were glad to welcome many contributions from other research worksers in the field. The proceedings of the Workshop were published by Springer [GR01].

FIREworks also directly supported the Summer School on Modelling and Verifying Parallel Processes, held 19-23 June 2000, in Nantes, France, by providing student grants. Several FIREworks members gave invited talks. The proceedings of this Summer School are currently in print.

Other FIREworks meetings took place, as summarised in the table below.

Date	Location	Participating sites
July 99	Trento	BHAM IRST FUNDP MAGD
Aug 99	Eindhoven	BHAM AALB
Sept 99	Zaragoza	BHAM LFCS
Sept 99	Toulouse	IRST NANT LaMI
March 00	Berlin	BHAM NANT LaMI
May 00	Glasgow (WS3)	BHAM GREN LFCS NANT FUNDP LaMI
June 00	Nantes (MOVEP)	BHAM AALB IRST FUNDP

FIREworks Visits

FIREworks members actively visited each other for short and medium periods to do colaborative work, as summarised by this table.

Date	Visit by	Visit to	Days	Persons
June 99	LFCS	IST	8	Ms. Kirli
July 99	MAG	NANC	9	Maritta Heisel
July 99	LaMI	Bham	6	H. Jouve, M. Aiguier, C. Gaston
July 99	NANT	BHAM	8	Franck Cassez
July 99	FUNDP	BHAM	19	Pierre-Yves Schobbens
Nov 99	FUNDP	LaMI	4	Pierre-Yves Schobbens
Nov 99	NANT	AALB	20	Franck Cassez
May 00	FUNDP	BHAM	8	Pierre-Yves Schobbens
July 00	FUNDP	BHAM	8	Pierre-Yves Schobbens
Aug 00	NANT	BHAM	7	Franck Cassez
Aug 00	LaMI	BHAM	3	Christophe Gaston
Oct 00	LaMI	FUNDP	2	1 person

Bibliography

ABE00: P. Abdulla, P. Bjesse, and N. Eén.
Symbolic reachability analysis based on SAT-solvers.
In Susanne Graf and Michael Schwartzbach, editors, Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00), volume 1785 of LNCS, Berlin, Germany, 2000. Springer-Verlag.
AHK97: R. Alur, T.A. Henzinger, and O. Kupferman.
Alternating-time temporal logic.
In Proceedings of the 38th Annual Symposium on Foundations of Computer Science, pages 100-109. IEEE Computer Society Press, 1997.
ASa: N. Aoumeur and G. Saake.
Consistency management in runtime evolving concurrent information systems : A co-nets-based approach, in proc. of the 9th international workshop on foundations of models and languages for data and objects: Database schema evolution and meta-modeling, dagstuhl, germany, 2000.
ASb: N. Aoumeur and Gunter Saake.
Distributed systems specification and runtime manipulation of their features using co-nets: Application to a system with several lifts, technical report, 2001.
BCCZ99a: A. Biere, A. Cimatti, E. Clarke, and Y. Zhu.
Symbolic Model Checking using SAT procedures instead of BDDs.
In Proceedings of the 36th Design Automation Conference (DAC'99), New Orleans, June 1999.
BCCZ99b: A. Biere, A. Cimatti, E. Clarke, and Y. Zhu.
Symbolic Model Checking without BDDs.
In Proceedings of the Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99), Amsterdam, the Netherlands, March 1999.
BGK01: K. Berkani, P. Le Gall, and F. Klay.
An incremental method for the design of feature oriented systems, chapter Algebraic Treatment of Feature-oriented Systems.
Springer-Verlag London Ltd, 2000/2001.
Cal00: C. Caleiro.
Combining Logics.
PhD thesis, IST, Universidade Técnica de Lisboa, 2000.
Supervised by A. Sernadas. Awaiting examination.
CCGR99: A. Cimatti, E.M. Clarke, F. Giunchiglia, and M. Roveri.
NUSMV: a new Symbolic Model Verifier.
In Eleventh Conference on Computer-Aided Verification (CAV'99), Trento - Italy, July 1999.
CCGR00: A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri.
NUSMV: a New Symbolic Model Checker.
Software Tools for Technology Transfer (STTT), 2:410-425, 2000.
CGHR00: G. Clark, S. Gilmore, J. Hillston, and M. Ribaudo.
Exploiting modal logic to express performance measures.
In B.R. Haverkort, H.C. Bohnenkamp, and C.U. Smith, editors, Computer Performance Evaluation: Modelling Techniques and Tools, Proceedings of the 11th International Conference, number 1786 in LNCS, pages 211-227, Schaumburg, Illinois, USA, March 2000. Springer-Verlag.
CGR⁺00: A. Cimatti, E. Giunchiglia, M. Roveri, R. Sebastiani, and A. Tacchella.
NuSMV Version 2: BDD-based + SAT-based Symbolic Model Checking.
Technical Report 12-40, IRST, Trento, Italy, December 2000.
Submitted for publication.
Cim01: A. Cimatti.
Industrial applications of model checking.
In MOVEP'2k, LNCS Tutorial Series, 2001.
To appear.
CL00: Franck Cassez and Kim G. Larsen.
The impressive power of stopwatches.
In Dale Miller and Catuscia Palamidessi, editors, CONCUR'00: Concurrency Theory, 11th International Conference on Concurrency Theory, volume 1877 of LNCS, pages 138-152, Penn-State Univ., Pennsylvania (USA), January 2000. Springer-Verlag.
ISBN 3-540-67897-2.
CM00: M. Calder and E. Magill, editors.
Feature Interactions in Telecommunications and Software Systems VI. IOS Press, 2000.
CMSS00: M. E. Coniglio, A. T. Martins, A. Sernadas, and C. Sernadas.
Fibring (para)consistent logics.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2000.
Extended abstract. Presented at II World Congress on Paraconsistency - WCP'00.
CR99: A. Cimatti and M. Roveri.
Conformant Planning via Model Checking.
In Proceedings of the 5th European Conference on Planning (ECP'99), 1999.
CR00: A. Cimatti and M. Roveri.
Conformant planning via symbolic model checking.
Journal of Artificial Intelligence Research (JAIR), 13:305-338, 2000.
CRS01a: F. Cassez, M. D. Ryan, and P.-Y. Schobbens.
Proving feature non-interaction using alternating-time temporal logic.
In Gilmore and Ryan [GR01].
CRS01b: Franck Cassez, Mark Dermot Ryan, and Pierre-Yves Schobbens.
Proving feature non-interaction with Alternating-Time Temporal Logic.
In Stephen Gilmore and Mark Ryan, editors, Language Constructs for Describing Features, pages 85-104. Springer-Verlag London Ltd, 2000/2001.
dAKN⁺00: Luca de Alfaro, Marta Kwiatkowska, Gethin Norman, David Parker, and Roberto Segala.
Symbolic model checking of concurrent probabilistic systems using MTBDDs and the Kronecker representation.
In Proceedings, TACAS'2000, volume 1785 of Lecture Notes in Computer Science, pages 395-410. Springer-Verlag, 2000.
dB99a: L. du Bousquet.
Feature interaction detection using testing and model-checking, experience report.
In World Congress on Formal Methods, Toulouse, France, September 1999.
dB99b: L. du Bousquet.
Validation incrémentale de services téléphoniques.
Phd thesis, Université Joseph Fourier, Grenoble, France, september 1999.
dBORZ98: L. du Bousquet, F. Ouabdesselam, J.-L. Richier, and N. Zuanon.
Incremental feature validation : a synchronous point of view.
In Feature Interactions in Telecommunications Systems V, pages 262-275. IOS Press, 1998.
dBORZ99: L. du Bousquet, F. Ouabdesselam, J.-L. Richier, and N. Zuanon.
Lutess: a specification-driven testing environment for synchronous software.
In 21st International Conference on Software Engineering, pages 267-276. ACM Press, May 1999.
dBORZ00: L. du Bousquet, F. Ouabdesselam, J.-L. Richier, and N. Zuanon.
Feature interaction detection using synchronous approach and testing.
Computer Networks and ISDN Systems, 32(4), April 2000.
dBZ99: L. du Bousquet and N. Zuanon.
An overview of lutess, A specification-based tool for testing synchronous software.
In 14th IEEE International Conference on Automated Software Engineering. IEEE, October 1999.
FC00: K.G. Larsen F. Cassez.
The Impressive Power of Stopwatches.
In Proceedings of CONCUR 2000-11th International Conference on Concurrency Theory, volume 1877 of Lecture Notes in Computer Science, pages 138-152. Springer, 2000.
FHP00: Laurent Ferier, Patrick Heymans, and Michael Petit.
Some hints for a clarification of cen env 12204.
In Proceedings of the Workshop on Evolution in Enterprise Engineering and Integration (to be published), Berlin, Germany, May 24-26 2000.
GAG00: C. Gaston, M. Aiguier, and P. Le Gall.
Algebraic treatment of feature-oriented systems.
Rapport interne numéro 44-2000, LaMI-Université d'Évry-val-d'Essonne, Janvier 2000.
GAG01: C. Gaston, M. Aiguier, and P. Le Gall.
Language Constructs for Describing Features, chapter Algebraic Treatment of Feature-oriented Systems, pages 105-124.
Springer-Verlag London Ltd, 2000/2001.
GH99: S. Gilmore and J. Hillston.
A feature construct for PEPA.
In N. Davies and J. Bradley, editors, Proceedings of the Fifteenth UK Performance Engineering Workshop, Department of Computer Science, The University of Bristol, July 1999.
GH00: Stephen Gilmore and Jane Hillston.
Performance modelling in PEPA with higher-order functions.
pages 35-46, 2000.
GH01: Stephen Gilmore and Jane Hillston.
The PEPA feature construct.
In Stephen Gilmore and Mark Ryan, editors, Language Constructs for Describing Features, pages 125-142. Springer-Verlag London Ltd, 2001.
GR01: Stephen Gilmore and Mark D. Ryan, editors.
Language Constructs for Describing Features. Springer-Verlag, 2001.
HHJP99: P. Haumer, P. Heymans, M. Jarke, and K. Pohl.
Bridging the gap between past and future in re : a scenario-based approach.
In K. Ryan, editor, Proc. of the Fourth IEEE International Symposium on Requirements Engineering (RE'99), pages 66-73. IEEE CS Press, june 1999.
Hil01: J. Hillston.
FMPA Lecture Notes, chapter Exploiting Structure in Solution: Decomposing Composed Models.
Springer-Verlag, 2001.
Hun99: J. Hunter.
Re-evaluation of the PEPA Workbench.
Master's thesis, School of Computer Science, The University of Edinburgh, September 1999.
JLS00: H. E. Jensen, K. G. Larsen, and A. Skou.
Scaling up Uppaal - Automatic Verificationof Real-Time Systems using Compositionality and Abstraction.
In Proceedings Sixth International School and Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems,FTRTFT 2000, volume 1926 of Lecture Notes in Computer Science, pages 19-30. Springer, 2000.
KMMR00: M. Kolberg, E. Magill, D. Marples, and S. Reiff.
Results of the second feature interaction contest.
In Calder and Magill [CM00], pages 311-325.
KNSS99: Marta Kwiatkowska, Gethin Norman, Roberto Segala, and Jeremy Sproston.
Automatic verification of real-time systems with discrete probability distributions.
In J.-P. Katoen, editor, Proceedings, ARTS'99, volume 1601 of Lecture Notes in Computer Science, pages 75-95. Springer-Verlag, 1999.
KNSS00: M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston.
Verifying quantitative properties of continuous probabilistic timed automata.
In C. Palamidessi and D. Miller, editors, CONCUR 2000, volume 1877 of Lecture Notes in Computer Science, pages 123-137. Springer, 2000.
KNSS01: Marta Kwiatkowska, Gethin Norman, Roberto Segala, and Jeremy Sproston.
Automatic verification of real-time systems with discrete probability distributions.
Theoretical Computer Science, 286(1-2), 2001?
To appear.
Lou: H. Lourenço.
Topic: Hybrid systems.
PhD thesis, IST, Universidade Técnica de Lisboa.
In preparation - Supervised by A. Sernadas.
LS00: H. Lourenço and A. Sernadas.
An institution of hybrid systems.
In Didier Bert and Christine Choppy, editors, Recent Developments in Algebraic Development Techniques - Selected Papers, volume 1827 of Lecture Notes in Computer Science, pages 219-236. Springer-Verlag, 2000.
Mat00: P. Mateus.
Interconnection of Probabilistic Systems.
PhD thesis, IST, Universidade Técnica de Lisboa, 2000.
Supervised by A. Sernadas and C. Sernadas. Awaiting examination.
McM93: K.L. McMillan.
Symbolic Model Checking.
Kluwer Academic Publ., 1993.
MMN⁺00: P. Mateus, M. Cabral Morais, C. Nunes, A. Pacheco, A. Sernadas, and C. Sernadas.
Randomly timed automata.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, March 2000.
Submitted for publication.
MPP⁺00: P. Mateus, A. Pacheco, J. Pinto, A. Sernadas, and C. Sernadas.
Probabilistic situation calculus.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, March 2000.
Submitted for publication.
MSS00: P. Mateus, A. Sernadas, and C. Sernadas.
Realization of probabilistic automata: Categorical approach.
In Didier Bert and Christine Choppy, editors, Recent Developments in Algebraic Development Techniques - Selected Papers, volume 1827 of Lecture Notes in Computer Science, pages 237-251. Springer-Verlag, 2000.
NR00: U. Nestmann and A. Ravara.
What's tyCO, after all?
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2000.
Short abstract. Presented at Express'00, satellite event of CONCUR'00.
Oua99: F. Ouabdesselam.
Feature interaction detection using a synchronous approach and testing.
In 2nd conf. on Quantitative Management in Software Engineering, Rome, Italy, December 1999. Ericsson.
Invited talk.
Pet99: Michael Petit.
A multi-formalism reuse-based approach to manufacturing systems modeling.
In Proc. of the International Enterprise Modeling Conference (IEMC'99), Verdal (Norway), June 14-16 1999.
PHS99: Michael Petit, Patrick Heymans, and Pierre-Yves Schobbens.
Agents as a key concept for information systems requirements engineering.
In Proc. of the International Bi-Conference Workshop on Agent-Oriented Information Systems (AOIS'99), Seattle (USA) and Heidelberg (Germany), May and June 14-15 1999.
Pla00: Malte Plath.
Language Constructs for Defining Features for Reactive Systems.
PhD thesis, School of Computer Science, University of Birmingham, 2000.
PR99: M. C. Plath and M. D. Ryan.
Feature integration using a feature construct.
To appear in Science of Computer Programming, Elsevier Publishing, 1999.
PR00: M. C. Plath and M. D. Ryan.
The feature construct for smv': Semantics.
In Magill and Calder [CM00].
PR01: M. Plath and M. D. Ryan.
Defining features for CSP: Reflections on the feature interaction contest.
In Gilmore and Ryan [GR01].
PSSM99: J. Pinto, A. Sernadas, C. Sernadas, and P. Mateus.
Non-determinism and uncertainty in the Situation Calculus.
In A. Kumar and I. Russell, editors, Proceedings of the FLAIRS'99 - the 12th International Florida AI Research Symposium, pages 454-460. AAAI Press, 1999.
Short version of [PSSM00].
PSSM00: J. Pinto, A. Sernadas, C. Sernadas, and P. Mateus.
Non-determinism and uncertainty in the Situation Calculus.
International Journal of Uncertainty, Fuzziness and Knowledge-Based Systems, 8(2):127-149, 2000.
Full version of [PSSM99].
Ram00: J. Ramos.
The Situation and State Calculus: Specification and Verification.
PhD thesis, IST, Universidade Técnica de Lisboa, 2000.
Supervised by A. Sernadas.
Rav00: A. Ravara.
Typing Non-uniform Concurrent Objects.
PhD thesis, IST, Universidade Técnica de Lisboa, 2000.
Supervised by V. Vasconcelos and A. Sernadas. Awaiting examination.
Res99: P. Resende.
Quantales, concurrent observations and event structures.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 1999.
Submitted for publication.
Res00: P. Resende.
Quantales and observational semantics.
In B. Coecke, D. Moore, and A. Wilce, editors, Current Research in Operational Quantum Logic: Algebras, Categories and Languages, volume 111 of Fundamental Theories of Physics, pages 263-288. Kluwer Academic Publishers, 2000.
Invited paper.
RL99: A. Ravara and L. Lopes.
Programming and implementation issues in non-unifom tyCO.
Technical report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 1999.
Presented at OOSDS'99 (Satellite Event of ICFP'99), Paris.
Ros97: A. W. Roscoe.
The Theory and Practice of Concurrency.
Prentice Hall, 1997.
RRV99: A. Ravara, P. Resende, and V. Vasconcelos.
An algebra of behavioural types.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 1999.
Submitted for publication.
RSSV00: J. Rasga, A. Sernadas, C. Sernadas, and L. Viganò.
Fibring labelled deduction systems.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, May 2000.
Submitted for publication.
RV00a: A. Ravara and V. Vasconcelos.
Typing non-uniform concurrent objects.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2000.
Extended version of [RV00b].
RV00b: A. Ravara and V. Vasconcelos.
Typing non-uniform concurrent objects.
In C. Palamidessi, editor, CONCUR'00, volume 1877 of Lecture Notes in Computer Science, pages 474-488. Springer-Verlag, 2000.
Short version of [RV00a].
SM99: L. Schröder and P. Mateus.
Universal aspects of probabilistic automata.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 1999.
Submitted for publication.
Spr00: Jeremy Sproston.
Decidable model chceking of probabilistic hybrid automata.
In M. Joseph, editor, Proceedings of the 6th International School and Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'00), volume 1926 of Lecture Notes in Computer Science, pages 31-45. Springer-Verlag, 2000.
TH00: J. Tomasik and J. Hillston.
Transforming PEPA models to obtain product form bounds.
Technical Report EDI-INF-RR-0009, Laboratory for Foundations of Computer Science, The University of Edinburgh, February 2000.
TSC: C. Türker, G. Saake, and S. Conrad.
Evolving objects: Conceptual description of adaptive information systems. in: Database schema evolution and meta modeling (demm'2000), ninth international workshop on foundations of models and languages for data and objects, schloss dagstuhl, germany, september 18-21, 2000.
VR99: V. Vasconcelos and A. Ravara.
Comunication errors in the pi-calculus are undecidable.
Information Processing Letters, 71:229-233, 1999.
Wan00: F. Wan.
Extending the PEPA Workbench solution methods.
Master's thesis, School of Computer Science, The University of Edinburgh, September 2000.
YO98: Yoneda and Ohta.
A formal approach for definition and detection of feature interaction.
In Feature Interaction in Telecommunications and Software Sytems (FIW 98), pages 202-216, 1998.
Zav98: P. Zave.
Architectural solutions to feature-interaction problems in telecommunications.
In Feature Interaction in Telecommunications and Software Sytems (FIW 98), pages 10-22, 1998.
Zua00: N. Zuanon.
Test de spécifications de services de télécommunication.
Phd thesis, Université Joseph Fourier, Grenoble, France, June 2000.

About this document ...

This document was generated using the LaTeX2HTML translator Version 98.1p1 release (March 2nd, 1998)

The command line arguments were:
latex2html -split 0 Report3.tex.

The translation was initiated by Mark D Ryan on 2001-05-26

Mark D Ryan
2001-05-26