Download this document as dvi file or gzipped PostScript.

Feature Integration in Requirements Engineering

Working Group 23531

Technical Report for Year 1

May 1998

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 first year report.

Importance and industrial relevance.

Complex software systems nearly always have an extended lifetime during which requirements change, e.g. because users become more sophisticated or because the underlying technology supports more capabilities. Meeting new requirements means adding features to the software systems; this may involve changing existing components or adding new components. The more complex the system, the harder it is to make such changes without breaking something; this problem has been dubbed the `feature interaction problem' in telecommunications. Methods and supporting tools to overcome these problems are of immense potential commercial value.

To guarantee industrial relevance of the work carried out by the Working Group, each academic partner is supported by a local industrial company, which is involved in the production or use of feature-oriented software. The supporters are mostly telecom companies.

The Working Group aims to extend some existing specification languages by adding feature-oriented constructs. It investigates validation, verification, and simulation methods for the extended languages and assesses their success via case studies.

Participants.

BHAM: The University of Birmingham (School of Computer Science), UK. Coordinating site. Participants: Mark Ryan (project coordinator), Marta Kwiatkowska.
AALB: Aalborg University (Department of Computer Science), Denmark. Participants: Arne Skou, Kim Larsen.
FUNDP: Facultés Universitaires Notre Dame de la Paix (Institut d'Informatique), Namur, Belgium. Participants: Pierre-Yves Schobbens, Eric Dubois and Philippe Du Bois.
IRST: Istituto Trentino di Cultura (Istituto per la Ricerca Scientifica e Tecnologica), Trento, Italy. Participants: Alessandro Cimatti, Fausto Giunchiglia.
IST: Instituto Superior Técnico (Departamento de Matemática), Lisbon, Portugal. Participants: Amílcar Sernadas and Cristina Sernadas.
LAMI: Université d'Evry (Laboratoire de Mathematiques et d'Informatique), France. Participants: Gilles Bernot.
LFCS: University of Edinburgh (Laboratory for Foundations of Computer Science) UK. Participants: Stephen Gilmore, Don Sannella.
MAD: Universidad Politécnica de Madrid (Departamento Ingeniería de Sistemas Telemáticos and ETSI Telecomunicación), Madrid, Spain. Participants: José Mañas, Tomás Robles Valladares.
MAG: University of Magdeburg (Institute for Technical Information Systems), Germany. Participants: Gunter Saake.
NANT: Ecole Centrale de Nantes (ICRyN), Nantes, France. Participants: Franck Cassez, Ahmed Bouabdallah.

Subgroups.

At the Initial Meeting (May 1997), subgroups were established as follows:

SG1 Model checking (<fireworks-sg1@cs.auc.dk>): Leader: Alessandro Cimatti
Model checking for feature interaction detection The feature construct in industrial strength model checker
SG2 Real-time and probabilistic logics (<fireworks-sg2@cs.auc.dk>): Leader: Marta Kwiatkowska
Probabilities to abstract from Intelligent Network complexity Feature interactions in real-time examples
SG3 Compositionality (<fireworks-sg3@cs.auc.dk>): Leader: Amilcar Sernadas Feature oriented spec vs OO spec FO relation with (standard) composition/abstraction Exploitation of FO by verification methods Combination of specifications and formalisms
SG4 Languages and tools (<fireworks-sg4@cs.auc.dk>): Leader: Pierre-Yves Schobbens
Which languages are suitable for extending with the feature construct? Defaults
SG5 Testing (<fireworks-sg5@cs.auc.dk>): Leader: Gilles Bernot
Testing techniques may be an efficient way to identify and study the critical modifications of behaviour induced by features. SG5 will investigate how far some classical testing techniques can be adapted to feature orientation.

Further details are available from the WWW page.

Summary and main conclusions

The first year of FIREworks has been a substantial success. An Initial Meeting was held in Namur, at which the member sites presented their technical background, and five subgroups were set up to facilitate co-operation. Since then, several visits and working meetings have taken place, and recently the first of three annual workshops has taken place in Magdeburg. (Details of these events are described in section 4. The first annual Workshop (WS1) is not described in this document since it occurred just after the end of the first year.)

Many papers have been published or are currently in progress (see References). Joint authorship across sites gives evidence of Co-operation between members, and this is anticipated to increase further during the life of the Working Group.

Research in First Year

AALB: Aalborg, Denmark

We have concentrated on the study of realistic industrial cases in order to gain insight in the problems when new features are added.

In [HLLS97] an existing real-time communications protocol for audio/video control is analysed in order to identify a design error. The problem was that messages occasionally were lost, and the company assumed that the loss was caused by unrecognised collisions on the shared system bus. The company was planning to enhance the system features, and in the new system a message loss would be fatal. In order to spot the error, a model of the existing implementation was built, and by sing the real-time model checker Uppaal, the timing error was identified, and a corrected version of the protocol was verified.
In order to build a model of a size that could be managed by the model checker, it was necessary to abstract away from irrelevant details such as message encoding, retransmissions etc. The case study indicated that it is possible to make such abstractions, and also that it is difficult to formalise such a notion of an appropriate abstraction.
The above case study was based on the analysis of an existing implemented system, and it would be interesting to see if a formal approach would be of use in the design phase as well. In order to make a further investigation of this question, it was agreed to collaborate on one of the new features in the extended system. In [HLS98] the result of this work is reported. The new feature consisted of a protocol for handling the automatic power up/down of the audio/video control system. In order to function properly, the powering sequence had to take place within given time limits.
A model was built of the new system, and in order to be manageable by the model checker, the existing system components had to be abstracted away as much as possible. It turned out that such abstractions were possible, and also that a formalisation of the abstraction notion was difficult to make.
By using the design model, it became possible to verify a number of desired design properties. In fact, it became clear that some of the properties were wrongly formulated. Also, some timing errors were identified and corrected.

BHAM: Birmingham, UK

We have developed a feature construct for the model checking language SMV, and use it to provide a plug-and-play framework for exploring feature interactions. We model the basic system and its features as different textual units, and integrate the features into the basic system, producing an extended system. We check for interactions by verifying the extended system. Although worked out in detail for SMV [McM93], this approach works in principle with any modelling language and verification method.

We have extended the SMV language with a new construct for describing features, and have built a prototype tool called SFI (``SMV Feature Integrator'') which compiles descriptions in this extended language into pure SMV, ready for verification by the SMV model checker. We present details of this extension and integration in our papers [PR98a,PR98b,Rya97], along with two substantial case studies of feature integration: the lift system, and the telephone system.

We have also worked on the foundations of probabilistic model model checking. The work has centred around the following themes: formulating probabilistic extensions of modal/temporal logics; constructing algorithms for automatic verification of probabilistic systems against probabilistic temporal logic specifications; and efficient data structures for probabilistic verification [HK97,BCHG⁺97,BKa,BK97a,BK97b,BKb].

Lastly, our work on the logical foundations of multi-agent systems is also related to features, since we are studying mechanisms for building highly expressive logics by adding off-the-shelf features to simple logics [LR98d,LR98b,LR97,LR98c,LR98a]

FUNDP: Namur, Belgium

The research of last year was centred on specification languages based on temporal logic. Features are indeed understood by the user from their temporal behaviour. One important aspect is that features modify specifications in a way that cannot be completely foreseen in advance. We have thus developed a logic for dealing with such evolving specifications, where time is divided in two levels: normal behaviour and exceptional changes of specifications due to feature additions [SSSS88]. Also, a complete system for a simple temporal logic was discovered [SR88]. We concentrated more specifically on real-time. In this field, we produced:

Complete proof systems for several real-time logics [RSH98];
A characterisation of the expressive power of these logics with respect to automata [HRS98]
A new compositional semantics for the real-time specification language Albert [FC98], allowing an easier link with the theoretical results.
A first attempt at developing a proof assistant based on PVS for the Albert language [Cha97].

This research work took place during the stay in Lisbon. Also during that time, a temporal non-monotonic logic was discussed with Sofia Guerra.

LFCS: Edinburgh, UK

Research on the feature interaction problem at the Edinburgh site has focussed on performance features (e.g., number of calls put through per minute; number of persons delivered to their desired destination, etc.). We have used stochastic process algebra to address these problems.

The focus for work on stochastic process algebra at the Edinburgh site is Performance Evaluation Process Algebra (PEPA) [Hil96]. PEPA allows the modeller to specify both behavioural aspects of a system and also performance-related measures. This gives a fresh perspective on feature interaction by providing a setting in which the impact of newly added functionality on measured system performance can be carefully analysed.

Our approach to defining the right conceptual structures and notation for the extension of PEPA for feature interaction analysis began by first developing a series of carefully measured models of feature interactions within different types of queueing systems [TH97]. The behaviour of simple computer systems which can be modelled by queues is a well-studied area from the performance perspective and provided a secure platform for the definition and consideration of a range of aspects of the feature interaction problem.

Adding new features to an existing complex system can have impact on both the functionality and the performance of the system and the new system is usually more complex than the previous one. This is the motivation for our continued research into novel techniques for state-space reduction via aggregation of a stochastic process algebra model and the classification of PEPA models into collections which yield to effective decomposition and solution techniques. We have completed our work on a new algorithm for efficient on-the-fly aggregation of PEPA models [GHR98] and have shown how the effective decomposition technique of quasi-separability can be applied to PEPA models [TGH98].

The PEPA language is supported by a suite of modelling tools, the best known of which is the PEPA Workbench. The tools in the modelling suite allow the modeller to check both behavioural properties of models (such as freedom from deadlock) and performance ones (such as throughput and component utilisation). We have recently been extending the suite of tools to add more advanced modelling capabilities and have taken this opportunity to reflect on the use of the suite so far both by the developers of the PEPA language and by its users [CGHT98].

This background has allowed us to progress to a suitable extended modelling notation for feature-oriented analysis of PEPA models. This notation provides the modeller with the ability to make precise statements about the features of the system which have measurable performance impact [GH98].

IRST: Trento, Italy

The activity was mainly devoted to the investigation and development of automatic techniques and tools for the verification and validation of specifications written in different styles.

NUSMV: We have developed a general platform for model checking, called NUSMV [ CCGR98], starting from the SMV system developed at CMU [ McM93]. The idea is that should be usable, customisable and extensible, with as little effort as possible, also by people different from the developers. A further goal is to produce a system which is very robust, and close to the standards required by industry. includes a number of extensions, a user interface, and several partitioning techniques which allow to tackle the state explosion problem. NUSMV will be used as the basis for a model checker for the verification and validation of feature oriented specifications and models.
Industrial applications: We investigated the applicability of different model checking systems to the verification and validation of a large, featured, industrial-scale designs [CGM⁺98a,HGCC⁺98,CGM⁺98b], i.e. part of the ``safety logic" of a railway interlocking system. The formal model is structured to retain the reusability and scalability properties of the system being modelled. Part of it is defined once for all at a low cost, and re-used. The rest of the model can be mechanically generated from the designers' current specification language. The model checker is ``hidden" to the user, it runs as a powerful debugger.
Planning via Model Checking: Planning via Model Checking is a novel approach to planning, firstly introduced in [CGGT97]. It is based on the reformulation of a planning problem to the exploration of a finite state automaton. Automata exploration can be efficiently performed with Model Checking, a formal verification technique widely applied in design of industrial systems. Planning problems are significantly difficult, and demand a thorough investigation of the state explosion problem. This approach was extended to solve more complex planning problems [CRT98b,CRT98a], and the application of abstraction techniques has begun to be investigated [CGR98].

IST: Lisbon, Portugal

The IST site has been involved in several tasks within the scientific range of FIREworks. The two talks delivered by IST at the FIREworks Initial Meeting in Namur, Belgium (May 23-24, 1997) focused on the relationship between model checking and theorem proving via synthesis, and on the algebraic characterisation of mechanisms for integrating heterogeneous specification logics. This second topic has, so far, materialised in three papers [SSC97b,SSC97c,SSC97a] and two MSc theses [Cou97,Nun98]. Categorical characterisations of synchronisation and fibring of logics were obtained and some preliminary preservation results were achieved. Temporalisation of logics has also deserved some attention. A systematic study of notions of logic and relation between logics was also developed.

The use of defaults in specification and their relationship to features are under current investigation in close collaboration with both Birmingham and Namur. Work on this area is reported in several papers [GRS97a,GRS97b,GR98,Gue98,sBRL98]. They focus, in particular, on default institutions as a means of structuring specifications and on the particular case of temporal logic. Some aspects of reasoning and applications to feature specification have also been addressed.

Research on the area of real-time and probabilistic logics is also ongoing. Preliminary results on the subject can be found in [Mat97,MSS98,LSS98] and will be presented at the forthcoming First FIREworks Workshop in Magdeburg, Germany (May 15-16, 1998). Although some aspects of model checking have been studied, the focus was, for now, on the semantics front.

Other approaches to the specification of reactive and concurrent systems have also been explored, namely temporal logic [CRSS98,DRCS97,ECSD98,SSC98], the situation calculus [Ram97], observational logic [Res97], and type theory [RV97a,RV97b]. Abductive reasoning within temporal logic has been studied in the submitted PhD thesis [Gou98].

LAMI: Evry, France

Our approach to the feature interaction problem is to use axiomatic specification formalisms in order to clearly identify interactions and, then generating test scenarii which give some concrete and relevant specified behaviours face to interactions.

The main reason for choosing axiomatic specifications is that we think it should be interesting to be able to identify the characteristics of the features involved ``as soon as possible.'' The high abstraction level of description allowed in axiomatic formalisms provide a good approach to specify interactions of features when they conceptually appear (in the right specification phase). Another reason for choosing axiomatic specification is that the modularity is well defined within axiomatic specification frameworks and although feature integration doesn't simply reduce to modularity problems, we hope to get benefits of this expertise.

Testing presents some advantages: for some years now, test sets have been automatically generated from specifications according to some coverage criteria, and test of non regression allows to check whether a new version of a software still remains successful w.r.t. a test set of the previous specification despite of the modifications. More specifically, testing and looking for interactions are activities which have some methodological similarities: while extracting test cases amounts to give particular cases which are error prone, locating interactions amounts to find particular cases which leads to unexpected behaviours.

We have worked on a specification of a lift managing system with some associated features in order to delimit the intrinsic problems of feature integrations and interactions. To perform this specification, we have chosen a real-time formalism developed at L.a.M.I. for its ability to include time and state notions within specification axioms. We have introduced some specification operators dedicated to specify features. Our specifications are composed of:

a main specification including two distinct sets of axioms. The first one will be preserved when integrating features. The second one specifies the minimal properties of the system under specification: these properties are required by default, without features;
a set of features including both the conditions of application of the considered feature and the characteristics of this feature.

From a semantic point of view, we are now beginning to describe features inside a two-level-specification framework: the first level specifies the real available code of the system while the second describes the user interface. The two levels are linked by the view the user has of the system. Subscribing a feature consists in applying a modifier on this view. A potential interaction of features will arise when the two features involved in the interaction impose two different views of a same user's functionality.

Moreover, we are also working on some subjects which, even if they are not directly connected to the feature area, will be re-used or adapted for feature issues:

Real-time specifications
It allows us to give an axiomatic semantic to the language VHDL devoted to programming/specifying hardware [BA97,Aig97]
Testing from formal specifications
We are investigating a way of defining logic-independent functional criteria and we are defining a testing method for object-oriented specifications (s.t. Etoile-specifications) [MAG96,MAG97,Aig97,GBB97,AG96]
Heterogeneous hierarchical specifications
We have defined syntax/semantic/proof aspects of a general framework of hierarchical specifications where each module is written according its own formalism. We are currently extending this framework to include heterogeneous and modular refinement.
Prototyping from formal specifications
Preliminary investigations are done in order to formalise the extraction of partial prototypes from specifications.

MAG: Magdeburg, Germany

We propose a method for the elicitation and the expression of requirements. The requirements can then be transformed in a systematic way into a formal specification that is a suitable basis for design and implementation of a software system. The approach - which distinguishes between requirements and specifications - gives methodological support for requirements elicitation and specification development. It does not introduce a new language but builds on known techniques [HS98].

Other members in MAG have continued work described in [CRSS97,CRSS98]. We introduce specification approach which allows to change the dynamic behaviour of objects in an information system during runtime of the system. For that we provide an extension of the specification language TROLL for adding and removing specification axioms (which, for instance, describe features of the system) by occurrences of special events, called ``mutators''. In this way, the set of axioms valid for the system may change in the course of time. In traditional specification approaches this is not possible: a modification of the valid axioms in a specification during runtime of the system usually results in inconsistencies or leads to the situation that the part of the system's life cycle already performed before the modification does not fulfill the modified specification. Our approach aims at at allowing dynamically adding new features to existing (and running) systems and dynamically changing or removing features currently present. As semantic basis we apply a two-layered approach based on OSL (Object Specification Language). In the base layer we use OSL for describing the part of the system's behaviour which is intended to remain always unchanged. On the meta level we have the changeable part of the specification as a set of currently valid axioms which are again expressed in OSL.

In [CS97] we present an alternative extension of temporal logic for describing evolving dynamic behaviour of objects in information systems.

In [TSC97] we present a case study in which we apply our specification approach [CRSS98]. As application area we choose federated (information) systems and we describe and discuss the dynamically adding of new component systems (and removing of currently present ones, as well). This case study had an essential influence on the shape of the specification language we use in [CRSS97,CRSS98].

Besides the research activities the Magdeburg group organised the 1998 FIREworks Workshop (May 15-16, 1998, Magdeburg). The proceedings of this workshop are available as [ST98].

NANT: IRCyN, Nantes, France

The activity within our team have concentrated on some of the objectives or the FIREworks project: investigating existing specification languages, logics and models and determine some of them capable of being extended with the notion of feature.

Our approach to the feature integration problem has been the following:

we have focussed on the modelling of features and feature integration; this part consisted in defining a suitable and rather general model (see [CB97] for details) to describe systems with features (more generally to which components may be added); this model is independent of any particular language. We also provided an integration operator on this model to define a semantic of the integration operation.
the above general framework has been the starting point of a case study with the system Promela/SPIN [Hol97]. The case-study we developed was the lift system [CB97,Cas98]. We have implemented the model as well as the integration operator within the Promela language for this example. Integration of various features was done this way together with feature interaction detection.
We are currently investigating the possibilities and limits of the I/O automata formalism [Lyn96] for addressing the problems of feature interaction and integration. The Lift System case study illustrates our approach [BC98].

Travel in first year

During the first year of FIREworks, the partners have worked hard at understanding the areas and opportunities for collaboration and therefore travel among the sites has been limited. The complexity of the topic has meant that sites have had to work hard on their own, but, as plainly established during the first annual workshop (WS1, Magdeburg, 15-16 May 1998) they are now ready to work together. There are several SG meetings and working visits in the planning stage, and it is expected that there will be more travel between the sites in the second year than the first; see section 5 on Future Plans.

Travel during the first year is as follows.

The Initial Meeting in Namur (May 22-24, 1997) was attended by Marc Aiguier, Gilles Bernot, Ahmed Bouabdallah, Wiet Bouma, Carlos Caleiro, Franck Cassez, Alessandro Cimatti, Marco Daniele, Gabriel Huecas, Marta Kwiatkowska, Malte Plath, Jean-Francois Raskin, Tomas Robles, Mark Ryan, Gunter Saake, Pierre-Yves Schobbens, Amilcar Sernadas, Arne Skou, Wiebe van der Hoek, Edwin Veenendaal, and Hugo Velthuijsen.
The agenda and minutes are attached as appendices to this document.
Pierre-Yves Schobbens ( FUNDP) has made a fruitful long visit to IST (September 1, 1997-January 30, 1998) during which several cooperation tasks were triggered. He made a further visit in April 1998. Topics discussed: temporal logic for evolving systems, proof systems for real-time temporal logics, combination of logics for specification.
J.-F. Raskin and J.-M. Zeippen ( FUNDP) visited the Trento site in June 1997. Topics: model checking, deduction, specification based on temporal logic.
The LAMI site met Franck Cassez and Ahmed Bouabdallah ( NANT) in Evry for a full day (5th May 1998) and presented their first version of feature formalisation. They discussed and compared this approach with the approach NANT takes in their previous works.

Future plans

Subgroup reorganisation.

It is in the nature of research activities that it is not possible to foresee what are fruitful avenues and connections, and therefore we should periodically review this subgroup structure and revise it where appropriate. After some email discussions, we decided that SG3(Compositionality) did not make very much sense as an independent subgroup, and that the members of SG3 should perform their investigations within the other subgroups. This decision was ratified at the Business Meeting in Magdeburg on 15 May 1998.

Planned research.

We report our future plans, according to the subgroups.

SG1

(Model checking)

Model checking techniques for feature-oriented specifications ( IRST, AALB, BHAM). The case studies developed within the first year of the project will be analysed in order to identify the bottlenecks of the current techniques.
Analysis of case studies with industrial partners ( AALB, BHAM)
New means to tackle the state explosion problem will be identified (eg, abstraction) ( AALB, BHAM, IRST)
Model checking performance features ( LFCS, IRST).
Extending PROMELA with a feature construct ( NANT, BHAM)

SG2

(Probabilistic and hybrid systems)

Continue current work on probabilistic and hybrid systems ( BHAM, IST).
Develop links with the Automatic Verification of Randomised Distributed Algorithms project at BHAM.

SG4

(Logics and tools)

Continue with work on defaults for expressing feature overriding ( IST, BHAM, FUNDP), particularly in temporal logics.
Real-time specification ( FUNDP); we also hope to develop more tools to support specification with the Albert language, and to see whether a more pragmatic support for features can be provided at the tool level. Specially, traceability and version/configuration tools might be extended to deal with features.
( LAMI) to modify our semantic grounds in order to be able to define a new feature in an already existing system. We would like to properly connect our syntactic and semantic choices, and to illustrate our approach on an example.
( MAG, NANT) Improve the heuristics for detecting interactions in our approach.
( NANT) Case studies at the Global Functional Plane level and the Distributed Functional Plane level of the Intelligent Network Conceptual Model [UT96], using verification tools developed at Muenchen University.
Continue to develop PEPA approach ( LFCS), concentrating on practical setting.
Develop temporal logics for capturing feature evolution ( MAG,IST), and continue with categorical techniques for combining logics and situation calculus ( IST).

SG5

(Testing)

Guide simulations to discover feature interactions ( NANT, LAMI, BHAM)
to define the first test scenarii for the LAMI approach.

Planned travel

Working Meetings in FIREworks are set up at relatively short notice within FIREworks, and therefore it is not possible to list all the meetings that will take place next year. The following meetings are planned, however:

IRST, BHAM, AALB. Topic: model checking features.
IST, BHAM. Topic: probabilistic logics.
LFCS, BHAM. Topic: performance features.
BHAM, NANT, LAMI: testing feature interactions.
BHAM, NANT: feature construct for PROMELA.
MAG, Nancy. Topic: methodology for feature integration
MAG will visit IST. Topic: Developing Temporal Logics for Capturing Evolution.
FUNDP will visit MAG.

The next Workshop (WS2) will be held on 9-10 April 1999, hosted by LaMI, Evry, France. It will be a joint Workshop with WG Esprit WG ASPIRE.

The third and final FIREworks Workshop (WS3) will take place in (approx) April 2000, hosted by IRST, Trento, Italy.

Bibliography

AG96: A. Arnould and P. Le Gall.
Formal specifications and test: Correctness and oracle.
In Springer-Verlag, editor, Recent Trends in Data Type Specification, number 1130 in Lecture Notes in Computer Science, pages 342-358. M. Haveraaen, 96.
abstract abbreviated (mcp).
Aig97: M. Aiguier.
ÉTOILE: a class-based logic with refinement.
Research Report 27, Laboratoire de Mathématiques et d'Informatique, Université d'Evry-Val d'Essonne, Cours Monseigneur Roméro, Evry, France, 1997.
Submitted for publication.
BA97: S. Béroff and M. Aiguier.
Spécifications algébriques temps réel.
Technique et Science Informatiques (TSI), 16(1/1997), 1997.
paper in french.
BC98: A. Bouabdallah and Franck Cassez.
I/o automata specification of lift services and additional features (in preparation).
Technical report, 1998.
BCHG⁺97: Christel Baier, Ed Clarke, Vasiliki Hartonas-Garmhausen, Marta Kwiatkowska, and Mark Ryan.
Symbolic model checking for probabilistic processes.
In Proceedings, 24th ICALP, volume 1256 of Lecture Notes in Computer Science, pages 430-440. Springer-Verlag, 1997.
BKa: Christel Baier and Marta Kwiatkowska.
Model checking for a probabilistic branching time logic with fairness.
Distributed Computing.
Accepted subject to revisions. Also available as Technical Report CSR-96-12.
BKb: Christel Baier and Marta Kwiatkowska.
On the verification of qualitative properties of probabilistic processes under fairness constraints.
Information Processing Letters.
Accepted subject to revisions.
BK97a: Christel Baier and Marta Kwiatkowska.
Automatic verification of liveness properties of randomized systems (extended abstract).
In Proceedings, Principles of Distributed Systems (PODC'97), pages 295-295. ACM Press, 1997.
BK97b: Christel Baier and Marta Kwiatkowska.
Domain equations for probabilistic processes (extended abstract).
In Proceedings, EXPRESS'97, volume 7 of Electronic Notes in TCS. Elsevier, 1997.
Full version submitted to Information and Computation, Technical Report CSR-97-7.
Cas98: Franck Cassez.
A model to describe feature integration.
submitted, April 1998.
CB97: Franck Cassez and Ahmed Bouabdallah.
Pragmatics for feature integration.
Technical Report RR97-11, IRCyN, 1 rue de la Noë, BP 92101, 44321 Nantes cedex 3, France, December 1997.
CCGR98: A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri.
NUSMV: a reimplementation of SMV.
Technical Report 9801-06, IRST, Trento, Italy, January 1998.
CGGT97: A. Cimatti, E. Giunchiglia, F. Giunchiglia, and P. Traverso.
Planning via Model Checking: A Decision Procedure for .
In Proceeding of the Fourth European Conference on Planning, Lecture Notes in Artificial Intelligence, Toulouse, France, September 1997. Springer-Verlag.
Also ITC-IRST Technical Report 9705-02, ITC-IRST Trento, Italy.
CGHT98: G. Clark, S. Gilmore, J. Hillston, and N. Thomas.
Experiences with the PEPA performance modelling tools.
In R. Pooley and N. Thomas, editors, Proceedings of the Fourteenth UK Performance Engineering Workshop, Edinburgh, Scotland, July 1998.
CGM⁺98a: A. Cimatti, F. Giunchiglia, G. Mongardi, D. Romano, F. Torielli, and P. Traverso.
Model Checking Safety Critical Software with SPIN: an Application to a Railway Interlocking System.
In Proceedings of the International Conference on Computer Safety, Reliability and Security (SAFECOMP98), October 1998.
To appear.
CGM⁺98b: A. Cimatti, F. Giunchiglia, G. Mongardi, D. Romano, F. Torielli, and P. Traverso.
Formal Verification of a Railway Interlocking System using Model Checking.
Technical report, IRST, Trento, Italy, April 1998.
Submitted to the Journal of Formal Aspects of Computing.
CGR98: A. Cimatti, F. Giunchiglia, and M. Roveri.
Abstraction in Planning via Model Checking.
In Proceedings of the Symposium on Abstraction, Reformulation and Approximation, SARA-98, Pacific Grove, California, May 1998.
Cha97: Francois Chabot.
Semantic embedding of albert-CORE within PVS.
Technical report, University of Namur, Computer Science Institute, 1997.
Published in the Proceedings of the Doctoral Consortium of the Third IEEE Symposium on Requirements Engineering (RE'97).
Cou97: M. J. Coutinho.
Estudo categorial do relacionamento entre Lógicas (A categorial study of relationships between logics).
Master's thesis, IST, Universidade Técnica de Lisboa, 1997.
In Portuguese - Supervised by C. Sernadas.
CRSS97: S. Conrad, J. Ramos, G. Saake, and C. Sernadas.
Evolving Logical Specification in Information Systems.
Preprint 5, Universität Magdeburg, Fakultät für Informatik, 1997.
CRSS98: S. Conrad, J. Ramos, G. Saake, and C. Sernadas.
Evolving logical specification in information systems.
In J. Chomicki and G. Saake, editors, Logics for Databases and Information Systems, chapter 7, pages 199-228. Kluwer Academic Publishers, Boston, 1998.
CRT98a: A. Cimatti, M. Roveri, and P. Traverso.
Automatic OBDD-based Generation of Universal Plans in Non-Deterministic Domains.
In Proceedings of the Fifteenth National Conference on Artificial Intelligence, Madison, Wisconsin, July 1998.
To appear.
CRT98b: A. Cimatti, M. Roveri, and P. Traverso.
Strong Planning in Non-Deterministic Domains via Model Checking.
In Proceeding of the Fourth International Conference on Artificial Intelligence Planning Systems (AIPS-98), Carnegie Mellon University, Pittsburgh, USA, June 1998. AAAI-Press.
CS97: S. Conrad and G. Saake.
Extending Temporal Logic for Capturing Evolving Behaviour.
In Z.W. Ras and A. Skowron, editors, Foundations of Intelligent Systems (Proceedings, 10th International Symposium, ISMIS'97, Charlotte, North Carolina, USA, October 1997), volume 1325 of Lecture Notes in Artificial Intelligence, pages 60-71, Berlin, 1997. Springer-Verlag.
DRCS97: G. Denker, J. Ramos, C. Caleiro, and A. Sernadas.
A linear temporal logic approach to objects with transactions.
In M. Johnson, editor, AMAST'97 - 6th International Conference on Algebraic Methodology and Software Technology, volume LNCS 1349, pages 170-184. Springer, 1997.
ECSD98: H.-D. Ehrich, C. Caleiro, A. Sernadas, and G. Denker.
Logics for specifying concurrent information systems.
In J. Chomicki and G. Saake, editors, Logics for Databases and Information Systems, chapter 6, pages 167-198. Kluwer Academic Publishers, Boston, 1998.
FC98: Jean-François Raskin François Chabot.
The formal semantics of albert.
Technical report, University of Namur, Computer Science Institute, 1998.
GBB97: P. Le Gall, G. Bernot, and L. Bouaziz.
A theory of probabilistic functional testing.
In Proc. of the Intl. Conf. on Software Engineering, 1997.
GH98: S. Gilmore and J. Hillston.
Feature interaction in PEPA.
In C. Priami, editor, Proceedings of the Fifth International Workshop on Process Algebra and Performance Modelling. Università di Verona, Italy, September 1998.
GHR98: S. Gilmore, J. Hillston, and M. Ribaudo.
An efficient algorithm for aggregating PEPA models.
Submitted for publication, 1998.
Gou98: P. Gouveia.
Raciocínio Abdutivo sobre Especificações Temporais de Objectos (Abductive Reasoning over Temporal Specifications of Objects).
PhD thesis, IST, Universidade Técnica de Lisboa, 1998.
Awaiting examination - In Portuguese - Supervised by C. Sernadas.
GR98: S. Guerra and M. Ryan.
Feature addition as composition of hierarchic default specifications.
In G. Saake and C. Türker, editors, FIREworks '98, Proceedings of the 1st FIREworks Workshop, Magdeburg, Germany, May 15-16, 1998, pages 14-29. Fakultät für Informatik, Universität Magdeburg, 1998.
GRS97a: S. Guerra, M. Ryan, and P.-Y. Schobbens.
Modular specifications with exceptions: on the properties of a default institution.
Technical report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1096 Lisboa, Portugal, 1997.
Submitted for publication.
GRS97b: S. Guerra, M. Ryan, and A. Sernadas.
Feature-oriented specifications.
Technical report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1096 Lisboa, Portugal, 1997.
Submitted for publication.
Gue98: S. Guerra.
Defaults in specifications: distance functions between temporal models.
In I. Kruijff-Korbayová, editor, Proceedings of the Third ESSLII Student Session, 1998.
HGCC⁺98: V. Hartonas-Garmhausen, S. Campos, A. Cimatti, E. Clarke, and F. Giunchiglia.
Verification of a Safety-Critical Railway Interlocking System with Real-time Constraints.
In Proceedings of the 28th International Symposium on Fault-Tolerant Computing (FTCS-28), Munich, Germany, June 1998. IEEE Computer Society Press.
Hil96: J. Hillston.
A Compositional Approach to Performance Modelling.
Cambridge University Press, 1996.
HK97: Michael Huth and Marta Kwiatkowska.
Quantitative analysis and model checking.
In Proceedings, 12th LICS, pages 111-122. IEEE Computer Society Press, 1997.
HLLS97: Klaus Havelund, Kim G. Larsen, Kristian Lund, and Arne Skou.
Formal modelling and analysis of an audio/video protocol: An industrial case study using uppaal.
In Proc. of the 18th IEEE Real-Time Systems Symposium, pages 2-13, December 1997.
HLS98: Klaus Havelund, Kim G. Larsen, and Arne Skou.
Formal verification of an audio/video power controller using the real-time model checker uppaal.
Submitted for publication, May 1998.
Hol97: Gerard Holzmann.
The model checker SPIN.
IEEE Transactions on Software Engineering, pages 279-295, May 1997.
HRS98: Thomas A. Henzinger, Jean-Francois Raskin, and Pierre-Yves Schobbens.
The regular real-time languages.
In Kim G. Larsen, editor, ICALP'98: 25th International Colloquium on Automata, Languages, and Programming, LNCS. Springer, 1998.
to appear.
HS98: Maritta Heisel and Jeanine Souquières.
Methodological support for requirements elicitation and formal specification.
In Proc. 9th International Workshop on Software Specification and Design, pages 153-155. IEEE Computer Society, 1998.
LR97: A. Lomuscio and M. Ryan.
On the relation between interpreted systems and Kripke models.
In Proceedings of the Workshop on Logical Approaches to Agent Modelling and Design at ESSLLI97 (European Summer School on Logic, Language, and Information), Aix en Provence, August 1997.
Technical Report CSR-98-1, School of Computer Science, University of Birmingham, UK. ftp://ftp.cs.bham.ac.uk /pub/authors/A.R.Lomuscio/esslli97.ps.
LR98a: A. Lomuscio and M. Ryan.
Ideal agents sharing (some!) information.
Technical Report CSR-98-1, School of Computer Science, University of Birmingham, UK, January 1998.
ftp://ftp.cs.bham.ac.uk/pub/tech-reports/1998/CSR-98-01.ps.gz.
LR98b: A. Lomuscio and M. Ryan.
Ideal agents sharing (some!) knowledge.
In Henri Prade, editor, Proceedings of Proceedings of the 13th European Conference on Artificial Intelligence, pages 557-561. John Wiley & sons, August 1998.
LR98c: A. Lomuscio and M. Ryan.
Model checking and refinement for S5_n.
In ECAI98 workshop on Practical Reasoning and Rationality, August 1998.
LR98d: A. Lomuscio and M. Ryan.
On the relation between interpreted systems and Kripke models.
In M. Pagnucco, W. R. Wobcke, and C. Zhang, editors, Agent and Multi-Agent Systems - Proceedings of the AI97 Workshop on the theoretical and practical foundations of intelligent agents and agent-oriented systems, volume 1441 of Lecture Notes in Artificial Intelligence, Berlin, May 1998. Springer Verlag, Berlin.
LSS98: H. Louren¸co, A. Sernadas, and C. Sernadas.
Aggregation and interconnection of hybrid automata: Categorial characterization.
In FIREworks '98, Proceedings of the 1st FIREworks Workshop, Magdeburg, Germany, May 15-16, 1998, pages 49-64. Fakultät für Informatik, Universität Magdeburg, May 1998.
Lyn96: Nancy A. Lynch.
Distributed Algorithms.
Morgan Kaufmann Publishers, 1996.
MAG96: B. Marre, A. Arnould, and P. Le Gall.
Dynamic testing from bounded data type specifications.
In Proc. of the second European Dependable Computing Conference, (EDCC-2), 96.
MAG97: B. Marre, A. Arnould, and P. Le Gall.
Giniration automatique de tests à partir de spicification de structures de donnies bornies.
In Actes des journees AFADL (Approches Formelles dans l'Assistance au Diveloppement de Logiciel), May 97.
Mat97: P. Mateus.
Categorial results in compositional model checking.
Technical report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1096 Lisboa, Portugal, 1997.
Diploma thesis - Supervised by A. Sernadas.
McM93: K.L. McMillan.
Symbolic Model Checking.
Kluwer Academic Publ., 1993.
MSS98: P. Mateus, A. Sernadas, and C. Sernadas.
Aggregation and interconnection of probabilistic automata: Categorial characterization.
In FIREworks '98, Proceedings of the 1st FIREworks Workshop, Magdeburg, Germany, May 15-16, 1998, pages 65-77. Fakultät für Informatik, Universität Magdeburg, 1998.
Nun98: A. L. Nunes.
Temporalização de Lógicas (Temporalisation of logics).
Master's thesis, IST, Universidade Técnica de Lisboa, 1998.
In Portuguese - Supervised by C. Sernadas.
PR98a: M. C. Plath and M. D. Ryan.
Plug-and-play features, 1998.
PR98b: M. C. Plath and M. D. Ryan.
A tool for adding features to systems described in the smv language, 1998.
Ram97: J. Ramos.
The situation and state calculus.
In A. Drewery, G.-J. Kruijff, and R. Zuber, editors, Proceedings of the Second ESSLII Student Session, 1997.
Res97: P. Resende.
Quantales, finite observations and strong bisimulation.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1096 Lisboa, Portugal, 1997.
Submitted for publication.
RSH98: Jean-Francois Raskin, Pierre-Yves Schobbens, and Thomas A. Henzinger.
Axioms for real-time logics.
In CONCUR'98: 9th International Conference on Concurrency Theory, LNCS. Springer, 1998.
to appear.
RV97a: A. Ravara and V. Vasconcelos.
Behavioural types for a calculus of concurrent objects.
In 3rd International Euro-Par Conference, volume 1300 of Lecture Notes in Computer Science, pages 554-561. Springer, 1997.
RV97b: A. Ravara and V. Vasconcelos.
A type algebra for concurrent objects.
Technical report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1096 Lisboa, Portugal, 1997.
Submitted for publication.
Rya97: M. D. Ryan.
Feature-oriented programming: A case study using the SMV language.
Technical report, School of Computer Science, The University of Birmingham, UK, September 1997.
sBRL98: F. M. Dionísio, S. Brass, M. Ryan, and U. Lipeck.
Hypothetical reasoning with defaults.
In Workshop on Computational Aspects of Nonmonotonic Reasoning - 7th International Workshop on Nonmonotonic Reasoning, 1998.
SR88: P.-Y. Schobbens and Jean-Francois Raskin.
Proving a conjecture of andreka on temporal logic.
Technical report, FUNDP and Instituto Superior Tecnico, 1988.
SSC97a: A. Sernadas, C. Sernadas, and C. Caleiro.
Fibring of logics as a categorial construction.
Technical report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1096 Lisboa, Portugal, 1997.
Submitted for publication.
SSC97b: A. Sernadas, C. Sernadas, and C. Caleiro.
Synchronization of logics.
Studia Logica, 59(2):217-247, 1997.
SSC97c: A. Sernadas, C. Sernadas, and C. Caleiro.
Synchronization of logics with mixed rules: Completeness preservation.
In M. Johnson, editor, AMAST'97 - 6th International Conference on Algebraic Methodology and Software Technology, volume LNCS 1349, pages 465-478. Springer-Verlag, 1997.
SSC98: A. Sernadas, C. Sernadas, and C. Caleiro.
Denotational semantics of object specification.
Acta Informatica, 1998.
In print.
SSSS88: Pierre-Yves Schobbens, Amilcar Sernadas, Cristina Sernadas, and Gunter Saake.
A two-level temporal logic for evolving specifications.
Technical report, FUNDP and Instituto Superior Tecnico, 1988.
ST98: G. Saake and C. Türker, editors.
FIREworks '98, Proceedings of the 1st FIREworks Workshop, Magdeburg, Germany, May 15-16, 1998. Fakultät für Informatik, Universität Magdeburg, May 1998.
TGH98: N. Thomas, S. Gilmore, and J. Hillston.
Applying quasi-separability to Markovian process algebra.
Submitted for publication, September 1998.
TH97: N. Thomas and J. Hillston.
Using Markovian process algebra to specify interactions in queueing systems.
Technical Report ECS-LFCS-97-373, Laboratory for Foundations of Computer Science, Department of Computer Science, The University of Edinburgh, 1997.
TSC97: C. Türker, G. Saake, and S. Conrad.
Modeling Database Federations in Terms of Evolving Agents.
In F. Pin, Z. W. Ras, and A. Skowron, editors, ISMIS 1997 -- Poster Proceedings of the 10th Int. Symposium on Methodologies for Intelligent Systems, Charlotte, North Carolina, October 15-18, 1997, pages 197-208. Oak Ridge National Laboratory, 1997.
UT96: Recommandations UIT-T.
Q.1213 : Global Functional Plane for Intelligent Network CS-1 - Q.1214 : Distributed Functional Plane for Intelligent Network CS-1.
1996.

Appendices

Program of FIREworks Initial Meeting

FIREworks: Initial Meeting. 23-24 May 1997, Namur, Belgium

Friday 23 May

10:00: Opening & welcome
10:30: BHAM - Marta Kwiatkowska: Probabilistic model checking
11:00: FUN - Pierre-Yves Schobbens: Decidable real-time logics
11:30: coffee/tea
12:00: IST - Amilcar Sernadas: Categorial characterisation of the fibring of logics
12:30: lunch in restaurant Les Combles, rue de l'Arsenal
2:00: Business meeting (agenda below)
3:00: coffee/tea
3:30: AALB - Arne Skou: Modelling and Verification Using UPPAAL: An Industrial Case Study
4:00: IST - Carlos Caleiro: Canonical operational semantics of temporal specifications
4:30: LaMI - Gilles Bernot: A Presentation of the Evry Team on Formal Specifications and Program Transformation
5:00: Reception
7:30: Dinner in Le Petit Brasseur, rue des Brasseurs

Saturday 24 May

9:00: BHAM - Mark Ryan: Features in SMV programs
9:30: BRST - Franck Cassez / Ahmed Bouabdallah: Examples of formal definitions of feature interactions
10:00: IRST - Alessandro Cimatti: Formal Methods at IRST: Research and technology transfer projects
10:30: tea/coffee
11:00: MAD - Tomas Valladares / Juan Quemada or Gabriel Huecas: E-LOTOS current state and future
11:30: KPN Research - Hugo Velthuijsen: Roadblocks on the path to automated feature interaction detection
12:00: lunch in Brasserie Henry, place Saint-Aubin
2:00: MAG - Gunter Saake: Temporal specification for evolving behaviour
2:30: Rijks Univ. Utrecht - Edwin Veenendaal : Features in Telecommunication Systems as Default Rules
3:00: Discussion

Minutes of First Business Meeting

FIREworks: Minutes of Initial Meeting. 23-24 May 1997, Namur, Belgium.

Present: Marc Aiguier, Gilles Bernot, Ahmed Bouabdallah, Wiet Bouma, Carlos Caleiro, Franck Cassez, Alessandro Cimatti, Marco Daniele, Gabriel Huecas, Marta Kwiatkowska, Malte Plath, Jean-Francois Raskin, Tomas Robles, Mark Ryan, Gunter Saake, Pierre-Yves Schobbens, Amilcar Sernadas, Arne Skou, Wiebe van der Hoek, Edwin Veenendaal, and Hugo Velthuijsen

1.

News of start date. 1 May 1997 was confirmed.

2.

Meetings and workshops. The following Workshops will be held.

15-16 May 1998:: Workshop 1, hosted by MAG, Magdeburg, Germany.
c. April 1999:: Workshop 2, hosted by LaMI, Evry, France, a joint Workshop with WG Exprit WG ASPIRE
c. April 2000:: Workshop 3, hosted by IRST, Trento, Italy.
Other meetings will be held on individual initiative (see WGP part 2).

3.

The subgroups were established. For each one, some potential issues were discussed. (See section 1 for list of subgroups.)

Membership of subgroups was agreed (please see WWW pages). additions/changes).

4.

Financial matters. It was agreed that the coordinating site holds all the money, and that expenses are paid by the coordinating site to the participant site in arrears. Participants in FIREworks events submit their expense claims to their own University, which (preferably in October and April each year) then claims the money from Birmingham University, by filing a financial report. (Birmingham can pay money only after it has received it from the Commission. The final 10% is not paid by the Commission until the final report has been accepted.)

Only travel and subsistence expenses for FIREworks meetings may be claimed (no overheads, but direct admin costs by the coordinating site are permitted). FIREworks meetings may conveniently be held next to another event, eg, a conference.

Each site will have one-tenth of 38.6 K Ecu in the first year; in the second and third years, the fraction of 38.6 K Ecu will be computed by a formula measuring the level of participation during the previous year, according to the weights:

Journal article 4 points
published Conf paper 3 points
Tech report 1 points
PhD thesis 2 points
presences at WS 2 points
presences at SG mtg 1 point
talks at WS 2 points
talks at SG mtg 1 point
SG leader 6 points

It was agreed that this formula would not be applied blindly, but that the coordinator will have the discretion to vary points or introduce minima/maxima in appropriate cases.

Papers must acknowledge and be relevant to FIREworks to count, and bibtex entry with URL must be submitted for annual report.

5.

Scientific reporting. LaTeX/BibTeX were agreed to be used throughout the WG.

(a)

Periodically, all members will send a BiBTeX entry for their FIREworks-relevant publications to Malte Plath (mcp@cs.bham.ac.uk), for inclusion on the WWW. The BiBTeX entry should include a URL field. Publications should bear acknowledgement for financial support to "Esprit WG FIREworks (23531)".

(b)

At the end of each year: each site will report its scientific results. Please \cite all of the papers you have submitted in (a).

(c)

each subgroup will report its scientific results, again citing the papers in (a).

(d)

each site reports the FIREworks activities in which it has participated, split into the categories:

Initial Meeting / Workshops
Working Meetings
Working visits to other sites
Validation meetings with industrial supporter (NB the last category is not funded by FIREworks)

(e)

The coordinator puts these together to form the annual report.

6.

Dissemination and Management. The tasks specified in the WGP which members have kindly agreed to carry out were confirmed.

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 Report1.tex.

The translation was initiated by Malte Plath on 1998-09-06

Page created by Malte Plath and maintained by Mark Ryan
Last modified: Oct 20, 2000

Journal article	4 points
published Conf paper	3 points
Tech report	1 points
PhD thesis	2 points
presences at WS	2 points
presences at SG mtg	1 point
talks at WS	2 points
talks at SG mtg	1 point
SG leader	6 points