Download this document as dvi file or as gzipped PostScript.

Feature Integration in Requirements Engineering


Working Group 23531


FIREworks




Technical Report for Year 2




June 1999

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


Contents

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

The previous 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.

Summary and main conclusions

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

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

Research in Second Year and Plans for Third Year

AALB: Aalborg, Denmark

The activities at Aalborg University during the second year are as follows:

Future work will include more industrial case studies and their impact on the Uppaal model checker.

BHAM: Birmingham, UK

We have primarily worked on developing the feature construct for SMV. This has involved developing our results from last year into a journal paper [PR99] (currently under review), and developing some of the theory of feature integration (paper in progress). We presented our work at the International Workshop on Feature Interactions [PR98a]. We also developed the feature construct for the Spin model checker [PR98b]. We had several meetings with our industrial supporter, British Telecom.

The work on probabilistic model checking reported last year has also continued [KNSS98,KNSS99]. The work continues to be centred around the following themes of constructing algorithms for automatic verification of probabilistic systems against probabilistic temporal logic specifications; and efficient data structures for probabilistic verification It has involved work on real-time systems, and systems involving continuous probability distributions.

We intend to explore guided simulation as an approach to scaling up our feature construct approach to the feature interaction problem. We will co-operate with the new Grenoble members of FIREworks for this.

Lastly, the work we reported last year on the logical foundations of multi-agent systems has continued. It has resulted in a successfully defended PhD thesis [Lom99], and also the papers [LR99a,LR99b,LR98]. Another FIREworks-related PhD thesis [Gue99] has been completed and will be examined in a few weeks.

FUNDP: Namur, Belgium

In Namur, our activities are related to the application real-time temporal logic results to requirements engineering, through the Albert II language and related tools. Most of our activity consists of developping tools to check adequacy and correctness criteria of Albert II specifications. This is an important basis for feature-oriented development, we believe, since features always ahve an important temporal aspect.

The Reasoning Assistant Tool

As mentioned in last year report, we are designing a toolset [JMZ98] to assist the analyst in his work of reasoning upon Albert II specifications. The support is basically methodological, in the sense that it is aimed at helping the analyst discovering the design of an argumentation. Over this year, we have been implementing a simple prototype of the toolset, which gave us interesting feedback on how to enhance it, in order to provide more effective support. A specification of a new version is underway.

The semantics

A number of basic investigations on the semantics of real-time languages [HRS98] have led to a complete axiomatization of the logic underlying Albert [Sch98,RSH98,SR99a]. As a side-effect, several known temporal logic has also been axiomatized [SR99b,SR98]. This also gives a decision procedure for this logic.

We also mentioned in the last year report that the semantics of Albert II had to be rewritten and, as a matter of fact, we wroate the semantics in a compositional style [CFRS99]. This allowed us to embed it in PVS whose purpose, when the embedding is complete, is two-fold:

This second point requires the definition of lemmas, theorems and strategies which shall help the specifier to prove the validity or invalidity of temporal formulae for a specification.

Albert II patterns for manufacturing systems

In the manufacturing domain, we investigated the use of the Albert II language to specify requirements on these systems. In these systems, the modeling of the interaction among distributed manufacturing equipment (machines of different kinds for processing, storing and transporting products) and distributed manufacturing software (mainly control software) is essential if one wants to investigate and ensure the correct behaviour of the system.

A set of specialised modeling patterns have been identified to quickly define the architecture of a manufacturing system in terms of a number of roles and/or agents (mainly equipment roles and control roles). Though these patterns allow to define a classical ``hierarchical'' control architecture, more interestingly they also allow to define formally a distributed control architecture. The proposed patterns are all defined on the basis of the Albert II language whose formal semantics allows unambiguous modeling and analysis the behaviour specification of the future system. A forthcoming PhD. thesis will report on the definition and usage of these patterns.

The animator

From the point of view of validation of distributed systems specifications, we developed an animator [HD99,HHJP99,PRB+98,HH98] for the Albert II language. The tool allows step-by-step testing of scenarios against the specification using an interpretation algorithm. As the specified system is distributed, the animation tool is also distributed: every participant in an animation session has to 'play the role' of one or more of the specification's agents, therefore allowing stakeholders to validate the components which are of interest for them and their interactions with the rest of the system. Other features of interest are as follows :

On-going and future work on the animator includes:

LFCS: Edinburgh, UK

Previous work on the investigation of the Feature Integration problem at Edinburgh had concentrated upon finding the right notion of equivalence between a system and its feature extension. The equivalence relations of classical process algeba are too discriminating for their application to this problem, judging systems to be not equal if they are not indistinguishable under observation. Or in the context of the timed process algebra which we use, PEPA, indistuishable under timed observation. Because PEPA is a Markovian process algebra, this relation is called Markovian Bisimulation.

A comparison of featured systems based on bisimulation is too uninformative, effectively only stating that a system and its feature extension are unequal. The Edinburgh site instead developed an expressive specification language for PEPA which could allow systems to be judged to be equivalent in some terms if they were as useful and as responsive, effected as passing a set of stochastic tests. This is a less strict, more useful notion for the investigation of the feature integration problem. The initial paper which presented the design of a specification language which included this notion of a feature-related equivalence was presented at the Magdeburg workshop and appeared in the proceedings of the Sixth International Workshop on Process Algebra Performance Modelling in September 1998 [GH98].

It would be an unwise practice to develop theoretical machinery without simultaneously testing its practical usefulness. This led to the production of a substantial case study which assessed the practical usefulness of the PEPA specification language. At the same time the authors related this novel description language to an existing logical formalism, Larsen and Skou's Probabilistic Modal Logic (PML). The paper on specifying performance measures in PEPA which included these two developments was presented in the AMAST Workshop on Real-Time Systems (ARTS '99) in May 1999 [CGH99].

In order to provide effective syntactic support for the description of features the Edinburgh site extended the language with a feature construct. 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 feature construct paper was presented at the Evry meeting and has been submitted to the Fifteenth Annual UK Performance Engineering Workshop to be held in September 1999 [GH99].

Forthcoming year of research at the Edinburgh site.

The coming year at the Edinburgh site will see further application of the newly created feature construct for PEPA, hopefully leading to publications of this work. At the same time, the PEPA tools will be extended and improved, in order to deliver effective support for the use of this linguistic construct in structured whole-lifecycle performance modelling of computer and telecommunications systems.

Other extensions of the PEPA modelling language are also being developed at Edinburgh: this has given rise to explicit language support for the composition of well-structured performance models [Cla99]. This was work discussed at the recent ARTS'99 meeting, also attended by the members of the FIREworks group from the Aalborg site. The syntactic characterisation of the class of models which can be solved efficiently has also been extended [HT98]. These extensions related to the FIREworks-relevant application area of featured models of computer systems.

The Edinburgh site will continue to develop its work on dynamic languages which are applicable to the problem of on-line detection of feature interactions [GKW97,WKG99,Wal99]. Some of this work has been presented at the recent workshop on Mobile Object Systems in Lisbon [Ki99] providing the opportunity for consultation between members of the Edinburgh site and the Lisbon site.

IRST: Trento, Italy

SMV NUSMV

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
In the first year, a general platform for model checking, called , was developed starting from the system developed at CMU [McM93]. The idea is that should be usable, customizable 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. In the second year, was extended with an interactive simulator and a graphical user interface [CCGR99,CCGR00]. 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 issues related to the applicability of model checking systems to the design and verification and validation of large, industrial-scale designs. The first is a vital protocol for point-to-point communications in distributed systems [CPS+99]. The second is a safety-critical control system for track-to-train communication [CCR+99]. In both cases, formal languages were used to detail the specifications, and model checking was used for early debugging and validation, pointing out several points of incorrectness and underspecification. Particular emphasis was devoted to the aspects of integration of the formal methodology within the software development cycle.
SAT-based Model Checking
A new techniques for symbolic model checking was developed [BCCZ99b,BCCZ99a]. The idea is to encode model checking problems in propositional calculus, in such a way that finding a counterexample to the model checking problem amounts to finding an assignment for a particular propositional formula. This task can then be performed with efficient, state of the art SAT solvers, and for certain applications is shown to outperform BDD-based decision procedures.

Planning via Model Checking
In the first year, the Planning via Model Checking approach was investigated. Basically, planning problems are reformulated as synthesis problems 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 second year, the theoretical properties of the formalism were investigated [DTV99]. Furthermore, the formalism was extended to deal with conformant planning problems [CR99], i.e. planning problems where no information is observabile at run-time.

Next year plan

The activity will aim at the integration of different techniques and tools for the verification and validation of feature-oriented specifications. The analyzed case studies have highlighted the relevance of verification techniques able to exploit the intrinsic hierarchical structure of the systems to be verified as a means to tackle the state explosion problem. Furthermore, the ability to validate imperative-style specification languages is badly needed. Future activity includes the investigation within of the results achieved out by the Birmingham group (development of a model checker for imperative programs) and by the Aalborg group (algorithms for verification of hierarchical systems). This will be carried out with meetings and visit exchange with Birmingham and Aalborg.

IST: Lisbon, Portugal

The activities of the IST site focused on logical approaches to system specification and verification, with emphasis on concurrency, distribution, hybrid and probabilistic aspects, defaults and abduction techniques. The group has been using and developing frameworks based on temporal logic, 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. Recent developments on some of these matters were addressed in the communications delivered by IST members at the ASPIRE/FIREworks Joint Workshop (April 8-10, 1999), held in Evry, near Paris, and also at several renowned conferences (among them: 13th International Workshop on Algebraic Development Techniques (WADT'98), 2nd International Workshop on Advances in Modal Logic (AiML'98), 25th International Colloquium on Automata, Languages, and Programming (ICALP'98) and 2nd International Workshop on Frontiers of Combining Systems (FroCos'98)).

With respect to temporal logic approaches, the current emphasis is on distribution [EC98], in close cooperation with Braunschweig, denotational semantics [SSC98], and evolving specification [SSSS98], in close cooperation with Namur and Magdeburg. Abduction techniques in this context have been developed in [Gou98], and were presented in [GS99]. Default specification and reasoning is another active topic of research with recent developments reported in [DBRL98,Gue99].

The situation calculus front was pursued with [RS99,PSSM99], the latter addressing also probabilistic issues. This line of research is the subject of [Ram] and has also driven some experiments using the COQ proof-assistant [Pac98,Car98,Pai98]. Further investigations on probabilistic systems are being pursued in [Mat] and recent developments can be found in [MSS99]. Hybrid systems and logics are also under investigation [Lou].

Other approaches to the study of concurrent systems are also under investigation: observational logic [Res99b,Res99a], and type theory [RRV98,Rav].

As far as combining logics is concerned, new results can be found in [ZSS99,SSCM99,CSS99,SSC99] and are the subject of [Cal].

Third Year Plan

The research plan for the next FIREworks year within the IST site consists mainly on the pursuit of the topics already outlined. Work will be directed to the study of categorial techniques for combining logics, specifications with defaults and their application to features, probabilistic and hybrid systems and logics, and general approaches to the specification of reactive and concurrent systems.

The combination of logics front will deal, namely, with the characterization of combination mechanisms for logics with algebraic semantics and the establishment of preservation results for them. This research is on the scope of one PhD thesis in preparation [Cal].

The development of logics for specifying and verifying both probabilistic and hybrid systems also falls within the scope of two other PhD theses being prepared [Mat,Lou]. The establishment of an approprate precategorial framework for this study is also under investigation.

Other topics include extensions of the situation calculus designed to deal with multi-agent state-based systems in the scope of another PhD thesis in preparation [Ram], and also issues related to probabilistic reasoning and abduction techniques.

Observational logic and type theory are another current interest, with ongoing research on their applications to concurrent, object-oriented, hybrid and real-time systems. A PhD thesis on this area is also in preparation [Rav].

LAMI: Evry, France

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

1.
We are currently investigating a proposition for a general framework dedicated to feature specifications. Our aim is to characterise as generally as possible the notion of features and of feature interaction. To reach this purpose, we tackle the problem both from the logic independent point of view and from the emerging property principle. Indeed, we aim to adapt our framework of hierarchical modular specifications [Cou98,CBG98] where a rule of property transmission from components to the global system is available. For features, the main difficulty is to define such a rule of property transmission from features to the global system because the monotony property is not systematically preserved for feature integration.
2.
From a pragmatic point of view, we are looking for defining for executable specifications (in the Prolog style) different strategies for integrating features. The idea of this work is to select from these specifications, some animations scenarii according to some well-chosen criteria. The resulting traces of these animations are submitted to an expert to decide among all detected interactions, the ones which are desirable and the ones which are undesirable. This process may be compared to a testing stage [MGB99,MGBB98].
We are also working on some subjects which are not directly connected to the feature interaction problem but are used or adapted for features issues:

MAD: Madrid, Spain

No activity was recorded, and no report was received. This team has effectively withdrawn from FIREworks.

MAG: Magdeburg, Germany

Based on our previous publications and research activities, e.g. [CRSS98], covering the topic of evolutionary specifications a new project related to the issues of FIREworks started by the end of 1998. The project ``Semantics of Adaptive Workflows (SAW)'' addresses adaptation and evolution in engineering applications, in particular for technical workflows. Based on a case study in a production environment, this project attempts to identify typical adaptation scenarios. Later on, these scenarios shall be covered by a newly created or extended specification language providing a formal semantics. Being part of the interdisciplinary project ``Integration of Specification Languages for Engineering Applications'' the SAW project is sponsered by the DFG (German Science Foundation). First results on some case studies have been presented and discussed on several project workshops.

Being the research focus of the Magdeburg group for several years now, Federated Database Systems (FDBS) represent a dedicated application scenario for feature interaction. Therefore a number of activities has taken place in this context, e.g. the GIM-approach [SS98] was developed, dependencies among nested transactions [STS98] in FDBS have been investigated, and the treatment of integrity constraints [TS99] was examined. Recently we successfully presented SIGMABench [HSC+99], a prototype of a FDBS design tool, which was developed to verify and demonstrate the mentioned approaches in practise. In future work we intend to incorporate special tools for analysing possible ``feature interaction'' problems occuring during the integration of existing databases (due to possibly contradictory information in the given database schemata, their integrity constraints, and the existing data stored in the preexisting systems).

Another topic of research is the investigation of the special case of specification of hardware protocols [Fis98,Fis99b]. For that special application field a modular approach [Fis99a] was proposed. Later, feature-orientation of that approach will be discussed.

In collaboration with the Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Nancy, France, an algorithm was developed to detect feature interactions in requirements. This algorithm is integrated in a method for systematic requirements elicitation [HS98c].

In our approach, features are modeled as sets of requirements. Requirements, in turn, are expressed in a schematic way, using predicate and event symbols. The algorithm for feature interaction detection works on that schematic representation of requirements. Given a new requirement and a set of already accepted requirements, the algorithm yields a subset of the accepted requirements that might interact with the new one. The algorithm, which is described in [HS98a,HS98b], is heuristic. This means that no guarantee can be given that all existing interactions are discovered.

Whereas the detection of interaction candidates is performed completely automatically, it is the task of the user to inspect the candidate set and decide whether there is an interaction or not. Resolution of detected interaction must also be performed manually. Further refinement of the algorithm and support for interaction resolution are subject of future work.

In addition to the projects already mentioned, several other research activities have taken place, mainly by scholarship holders working on topics closely related to FIREworks. For instance, structuring constraints of object oriented applications as first class citizens in object oriented data models and the feasibility of doing this by using basic notions of object orientation have been investigated [OCS99,OS98a,OS98b,OS98c,OS99] Other publications have dealt with object oriented specification languages and their transformation and formal semantics [AS99b,AS99a,AS99c,Aou99].

Ralf Pinger from the Braunschweig research group got in touch with Alessandro Cimatti from Trento on the Evry workshop and agreed that Ralf should visit Alessandro in Trento later this year, also to attend the model checking tutorium 2-4 July, and possibly the CAV conference 7-10 July.

NANT: IRCyN, Nantes, France

The activity within our team has continued 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.

We have used the framework we developped in [CB97,Cas98] on an example of a lift system [Cas99].

Our main concern is now to try and use infinite state machines to model the behaviour of featured systems and to see to what extent they can prove useful in the modelling and verification phases of such systems.

In [SFRC99], we have studied a model of infinite state machines, namely the FIFFO-automata, that can help in modelling and proving systems with unbounded number of event occurrences.

The use of timed automata and hybrid automata is also investigated in order to introduce timing constraints in the model of a featured system. We have hosted a working visit with FIREworks partners from Aalborg, focussed on verification of timed and hybrid automata. 8 talks were given from march, 30 to April 1st, 99 by the following participants: Kim Larsen (Aalborg, Denmark), Vlad Rusu (IRISA, Rennes, France), François Laroussinie (ENS, Cachan, France), Olivier Roux and Franck Cassez (IRCyN, Nantes, France).

Forthcoming and planned activities

Further work will consist in:

Visits

Franck Cassez and Ahmed Bouabdallah visited [EVRY] on may 5th, 1998. We have discussed issues on the modelization of integration of features.

A FIREworks working meeting took place in [NANT] from march, 30 to April 1st, 99. Apart from the FIREworks members Kim Larsen [AALB] and Franck Cassez [NANT], other participants were invited and gave talks. Hereafter is a list of the talks given:

We have also planned a working visit to [BHAM] in july 99 and another in [AALB] in the fall 99.

   
Travel in second year

We detail the principal events which took place.

WS1 at Magdeburg, Germany

Our First Workshop took place 15-16 May 1998 in the delightful setting of a manor house in Magdeburg, Germany, hosted by Gunter Saake and Can Türker. (Photos.)
There were approximately 16 talks and two discussion sessions. About 34 persons attended (including some locals). At least one of our industrial supporters was represented: Wiet Bouma from KPN Research came. 


Friday, May 15, 1998 


8.40		 Registration 


8.55		 Workshop opening (G. Saake and M. Ryan)  






Session 1 (chair: Gunter Saake) 


9.00		 Wiet Bouma: Feature Interactions:A Survey  


9.45		 Malte Plath: Plug and Play Features 


10.30		 Break 


10.45		  Franck Cassez: A Semantics for Feature Integration 


11.30		  Stephen Gilmore: Feature Interaction in PEPA 


12.15		 Lunch 






14.00		 Business meeting 






Session 2 (chair: Pierre-Yves Schobbens) 


14.30		   Maritta Heisel: Detecting Feature Interactions - A Heuristic Approach  


15.00		  Ahmed Bouabdallah: I/O Automata Specification of Lift Servicesand Additional Features   


15.30		 Break 


15.45		  Pascale Le Gall: Testing from Formal Specifications 


16.30		 Arne Skou: Formal Verification of an Audio/Video Power Controller using the Real-Time 
		 Model Checker Uppaal  


17.15		 Discussion  ``Testing and Simulation '' (chair: Gilles Bernot) 




Saturday, May 16, 1998 


Session 3 (chair: Malte Plath) 


9.00		  Gilles Bernot: A Two Level Specification of Features


9.30		  Hugo Lourenco: Aggregation and Interconnection of Hybrid Automata: Categorial 
		 Characterization 


10.00		 Pierre-Yves Schobbens: Real-time Specification  


10.30		 Break 






Session 4 (chair: Wiet Bouma) 


10.45		   Alessandro Cimatti: Abstraction in Planning via Model Checking 


11.30		  Marco Roveri: NuSMV: an Industrial Strength Model Checker 


12.00		  Mark Ryan: Semantics of the SMV Feature Construct 


12.30		 Lunch 






Session 5 (chair: Hans-Dieter Ehrich) 


14.00		  Sofia Guerra: Feature Addition as Composition of Hierarchic Default Specifications  


14.30		  Paulo Mateus: Aggregation and Interconnection of Probabilistic Automata: Categorial 
		 Characterization 


15.00		 Discussion  ``Verification '' (chair: Mark Ryan) 





16.00		 Closing of workshop



Business Meeting.

During this event, a business meeting also took place (14:00, 15 May 1998). The minutes are as follows:
1.
The healthy financial position was noted.
2.
Activity of partners. Some Partners appear to be inactive, while there are other groups working on features who are not members of the WG, but with whom we could usefully cooperate. It was agreed that we could decide to involve such groups by making them ``associate partners", attached to an existing site, and invite them to our meetings. Such a decision would be taken by email or at a Busines Meeting. It was decided to make the group of Jeanine Souquières in Nancy such a member, associated to NANT or LaMI.
3.
Subgroups. It was agreed to restructure the subgroups by removing SG3 (Compositionality) and including that activity in the remaining subgroups.
4.
Workshops were confirmed as follows:

FIREworks meeting at the Feature Interaction Workshop, Lund, Sweden, 29 September 1998

Present: M. Plath, M. Ryan (BHAM), M. Aiguier, P. LeGall, C. Gaston (LaMI), M. Heisel (MAG), L. du Bosquet, N. Zuanon, F. Ouabdesselam, J.-L. Richier (External: Grenoble), J. Bredereke (External: Ontario).

FIW'98 was the 5th of a series of international workshops on feature interaction. This year, its title was broadened from ``Feature Interactions in Telecommunication Systems" to ``... in Telecomunication and Software Systems", making it even more relevant to FIREworks. Full details of the programme are available from http://www.tts.lth.se:80/FIW98/.

Topics of discussion at FIREworks meeting:

There was also a presentation: Feature validation, by N. Zuanon, and an animated discussion following it.

Stochastic Modelling and Verification, Birmingham; 1-3 October 1998

Present: M. Ryan (BHAM), M. Kwiatkowska (BHAM), G. Norman (BHAM), J. Sproston (BHAM), D. Parker (BHAM), A. El-Rayes (BHAM), J. Hillston(LFCS), G. Clark (LFCS), P. Mateus (IST).

This was a joint FIREworks-SG2 and ARC meeting. Other ARC members present: C. Baier, B. Engelen Mannheim), U. Herzog, J.-P. Katoen, M. Siegle (Erlangen-Nurnberg).

Presentations:

FIREworks SG2 identified the themes (i) using probabilities to abstract from Intelligent Network complexity, and (ii) investigating feature interactions in real-time examples. Stochastic process algebras provide a probabilistic modelling framework in which the equivalence relations of process algebras can be used to reduce the size of Markovian process models, giving the desired reduction in the state-space of a model. This powerful abstraction device makes it possible to analyse models of a size and complexity beyond those for which conventional methods are applicable. The application to Intelligent Networks stems from Hillston and Clark's development (with Gilmore, also LFCS) of a feature-oriented notation which can be applied in the analysis of both the quality of service problems and the feature interaction problems which are known to arise in IN.

Abstracts of these talks can be found at http://www.cs.bham.ac.uk/~gxn/arcprogramme.html.

Visit by Patricia Machado to Evry to visit Gilles Bernot's group, November 1998

The topic of the meeting was on the use of test for verifying feature-oriented systems. Testing features must rely on invariant properties of the systems rather than on individual behaviour of components and on the interaction of features. Therefore, testing suites must be derived from a more abstract level than the one of communicating components. A method for testing feature-oriented systems is still needed and it will strongly depend on feature oriented constructions of the languages adopted. So far, feature-oriented specification languages have been investigated with the additional aim of producing testable systems with the capability of having new features added, combined and removed. Existing testing techniques will be taken into account when appropriate and adapted to encompass features.

FIREworks SG1 meeting, Amsterdam, March 24, 1999

The meeting was held in conjunction with ETAPS'99.

Attending: Alessandro Cimatti (IRST) (SG leader), Don Sannella (LFCS), Kim Larsen (AALB), Malte Plath (BHAM) (minutes).

Kim Larsen reported on a project with B&O, about adding a ``Power Down" feature to the protocol controlling B&O HIFI systems. Other work at AALB is concerned with model checking UML specifications with Uppaal.

We discussed the significance of research presented at TACAS, concerning reuse and compositionality of reachability results in verifying hierarchical state machines. It seems that this technique could greatly improve the analysis of featured systems when the results for base system are known. (``incremental verification")

Alessandro Cimatti gave a brief description of the model checker NuSMV (developed at IRST) and speculated about exploiting hierarchical structures in a similar way in NuSMV.

The next SG1 mtg will probably be held in conjunction with CAV'99, the 5th SPIN workshop, and the SMC workshop in Trento, Italy, in July 1999.

Visit by Kim Larsen to Nantes, 30 March / 1 April 1999

Present: KL=Kim Larsen, FL=Francois Laroussinie, FC=Franck Cassez, OR=Olivier Roux, VR=Vlad Rusu

Programme:

March 30 p.m.
14h30-15h30 FC: ``Hybrid FIFFO Automata" This talk will introduce the FIFFO automaton model which is derived from the FIFO one. We will describe existing results on this model, and further problems related to introducing constraints (e.g. via hybrid systems) on the environment of the FIFFO automata.

16h00-17h00 FL: ``Complexity of Model-Checking for Timed Modal Logics" This talk will present complexity results for model- checking of several fragments of the timed modal mu- calculus. The aim is to analyse precisely where the complexity blow-up (compared to untimed case) comes from.

March 31 a.m.
9h30-10h30 KL: ``UPPAAL, Current Developments and Applications" This talk will comment on the new graphical interface of UPPAAL, its recent applications in the Esprit Project VHS (Verification of Hybrid Systems), and future model checking techniques ported from results in a danish project VVS (Verification and Validation of Systems).

11h00-12h00 FL: ``Expressivity of Lnu, a timed modal logic" This talk will present Lnu, a timed modal logic used in the verification tool CMC (http://www.lsv.ens-cachan.fr/~fl). We will see the kind of property which can be expressed with Lnu (safety and bounded liveness, simulation of invariants and urgency, timed bisimulation).

March 31 p.m.
14h00-15h00 KL: ``Scheduling with timed automata"

15h00-16h00 VR: ``Symbolic test generation and abstraction"

- 16h30 Discussion

April 1st a.m.
- 9h30-10h30 OR: ``Splitting Analysis" A technique to compute the upper-approxiamtion of the set of reachable states of a synchronized product of hybrid automata.

- 11h00-12h00 KL: ``Clock Difference Diagrams" A new BDD-like datastructure for (certain) non-convex subsets of the Euclidean space.

April 1st p.m.
FL: talk in French for the IRCyN audience ``Vérification (compositionnelle) de systèmes temporisés"

WS2 at Evry, France

Our Second Workshop took place 8-10 April 1999 in Evry, France, and was a joint event with the ASPIRE Working Group, hosted by Gilles Bernot, Marc Aiguier, and Pascale LeGall. We had approximately 28 talks, including invited talks from

The workshop programme: PostScript


Business Meeting.

The business meeting held in Evry on 9th April 1999 had present: BHAM: M.Ryan (chair & secr), M.Plath; AALB: - ; FUN: - ; IRST: A.Cimatti; IST: F.M.Dionisio; LaMI: G.Bernot, M.Aiguier; LFCS: S.Gilmore; MAD: - ; MAG: S.Conrad, H-D.Ehrich, M.Heisel.

Minutes:

1.
Opening

2.
Cash flow: apologies and request. I aplogised for delays in BHAM refunding participating sites, and made two requests:
(a)
that you inform me when it happens, and I will chase;

(b)
that you ask your administrations to promptly process your requests for this year, including those relating to WS2 in Evry, so that we can file accurate accounts.

3.
Reports and publications for year 2. Malte Plath will soon ask participants for their reports of their Y2 activities and publications for the FIREworks pages.

4.
Budget. I reported underspending and we looked at ways of increasing activity levels, namely:

5.
We unanimously agreed to seek EC aproval to co-opt two further sites to FIREworks, namely
(a)
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
(b)
LORIA, Universite Henri Poincare, BP 239, 54506 Vandoeuvre, France. Site leader: Jeanine Souquieres
Other members: Dominique Mery

6.
Location and date of WS3. The default is Trento, as stated in the Proposal, and again offered by Alessandro Cimatti. However, we did not confirm it, because
(a)
we may prefer to hold WS+ instead in Trento (see item #7)
(b)
we may prefer to hold WS3 co-located with FIW'00 in Glasgow/Stirling.
(c)
Don Sannella suggests ETAPS'00 (Berlin, c. 25 March)
[Since the meeting, we decided to co-locate with FIW'00.]

7.
Additional workshop WS+. It was agreed that Mark Ryan would continue to work on the proposal of an additional workshop, with approximately the following profile.
(a)
Theme. Within the area of Specification and Verification of Featured Systems, interpreted broadly. A more precise theme/title for the workshop will be determined by the Program Committee (to be established).
(b)
Tutorials given by FIREworks members (dissemination of FW results, to be interpreted broadly).
(c)
Research presentations, to be given by invited speakers.
(d)
Duration: 3d.
(e)
Location: we have two offers: Trento, host Alessandro Cimatti; and Lisbon, host Amilcar Sernadas.
(f)
Time: June 00?
You are welcome to contact me if you have further ideas, offers, proposals etc. Otherwise, stand by for more information from me in the coming months.

Action: M.Ryan to continue working on the proposal.

8.
Forthcoming meetings. FLOC'99: FIREworks meeting to be held 6th July; FM'99: FIReworks meeting to be held. Action: M.Ryan: seek approval from EC for meetings at non-sites; M.Heisel: propose date for FM'99 meeting.

9.
Closing.

  
Future plans

The final year of FIREworks should be an exciting one. We will hold our normal meetings and annual workshop WS3, and are investigating whether to plan an additional workshop WS+. The details will be discussed at a FIREworks meeting taking place in July in Trento. We also welcome additional partners in Grenoble and Nancy for the final year, following approval of our invitation by the Project Officer. So far there are several FIREworks meetings in the pipeline:

* denotes: permission from Project Officer currently being applied for.

Bibliography

Aou99
N. Aoumeur.
On the Semantics of Mondel Specification Using a Concurrent Object Petri Net-Based Approach.
Preprint 7, Fakultät für Informatik, Universität Magdeburg, 1999.

AS99a
N. Aoumeur and G. Saake.
Operational Interpretation of the Requirements Specification Language ALBERT Using Timed Rewriting Logic.
In Proc. of 5th Int. Workshop on Requirements Engineering: Foundation for Software Quality (REFSQ'99), Heidelberg, Germany, June 1999, 1999.
To appear.

AS99b
N. Aoumeur and G. Saake.
Towards a New Semantics for Mondel Specifications Based on the CO-Net Approach.
In Proc. Modellierung'99, Karlruhe, Germany, March 1999, pages 107-122. B. G. Teubner-Verlag, 1999.

AS99c
N. Aoumeur and G. Saake.
Towards an Object Petri Nets Model for Specifying and Validating Distributed Information Systems.
In Proc. of the 11th Int. Conf. on Advanced Information Systems Engineering, CAiSE'99, Heidelberg, Germany, Lecture Notes in Computer Science, Berlin, 1999. Springer-Verlag.
To appear.

BA97
S. Béroff and M. Aiguier.
Real time algebraic specifications.
Technical Report 23, LIVE/LaMI, 1997.

BA98
S. Béroff and M. Aiguier.
Spécifications algébriques temps réel.
Technique et Science Informatique, 17(1), 1998.

Bar98
D. Barhami.
Cadre général pour la logique équationnel.
Master's thesis, Université d'Evry val d'Essonne, LaMI, September 1998.

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.
To appear.

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.
To appear.

Bér99
S. Béroff.
Présentation d'un formalisme de spécification dynamique et temps réél: application à la sémantique du langage VHDL.
PhD thesis, Université d'Evry val d'Essonne, LaMI, Junuary 1999.

Cal
C. Caleiro.
Topic: Combination of logics.
PhD thesis, IST, Universidade Técnica de Lisboa.
In preparation - Supervised by A. Sernadas.

Car98
A. Carvalho.
Category theory in COQ.
Technical report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1096 Lisboa, Portugal, 1998.
Diploma thesis - Supervised by A. Sernadas and P. Mateus.

Cas98
Franck Cassez.
A semantic approach to feature integration.
First FIREworks Workshop, FIREworks'98, Magdeburg, Germany, 13-15 may 1998.

Cas99
Franck Cassez.
Operators for structuring feature integration.
submitted, 1999.

CB97
Franck Cassez and Ahmed Bouabdallah.
Pragmatics for feature integration.
Rapport de recherche 97-11, IRCyN, Ecole Centrale de Nantes, December 1997.
51 pages.

CBG98
S. Coudert, G. Bernot, and P. Le Gall.
Hierarchical heterogeneous specifications.
In Selected papers of the workshop on Abstract Data Types (WADT), number 1589 in LNCS, pages 106-120, 1998.

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), 2000.
To appear.

CCR+99
A. Chiappini, A. Cimatti, G. Rotondo, C. Porzia, R. Sebastiani, P. Traverso, and A. Villafiorita.
Formal Specification and Development of a Safety-Critical Train Management System.
In Proceedings of the 18th International Conference on Computer Safety, Reliability and Security ( SAFECOMP'99), Toulouse, FRANCE, September 27-29 1999.
To appear.

CFRS99
F. Chabot, L. Ferier, J.-F. Raskin, and P.-Y. Schobbens.
The formal semantics of Albert II.
Technical report, University of Namur, 1999.

CGH99
G. Clark, S. Gilmore, and J. Hillston.
Specifying performance measures for PEPA.
In J.-P. Katoen, editor, Proceedings of the Fifth International AMAST Workshop on Real-Time and Probabilistic Systems, Bamberg, Germany, May 1999.

Cla99
G. Clark.
Stochastic process algebra structure for insensitivity.
In J. Hillston, editor, Proceedings of the Seventh Annual Workshop on Process Algebra and Performance Modelling, pages 63-82, Zaragosa, Spain, September 1999.

Cou98
S. Coudert.
Hiérarchie et hétérogénéité dans les spécifications algebriques.
PhD thesis, Université d'Evry val d'Essonne, LaMI, December 1998.

CPS+99
A. Cimatti, P.L. Pieraccini, R. Sebastiani, P. Traverso, and A. Villafiorita.
Formal Specification and Validation of a Vital Communication Protocol.
In Proceedings of the FM99: World Congress on Formal Methods, Toulouse, France, September 1999.

CR99
A. Cimatti and M. Roveri.
Conformant Planning via Model Checking.
1999.
Submitted to the 5th European Conference on Planning.

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.

CSS99
C. Caleiro, C. Sernadas, and A. Sernadas.
Parameterisation of logics.
In J.L. Fiadeiro, editor, Recent Developments in Algebraic Development Techniques, Selected Papers, volume 1589 of Lecture Notes in Computer Science, pages 48-62. Springer-Verlag, 1999.
In print.

DBRL98
F. M. Dionísio, S. Brass, M. Ryan, and U. Lipeck.
Hypothetical reasoning with defaults.
In Ilkka Niemelä and Torsten Schaub, editors, Proceedings of the Workshop on Computational Aspects of Nonmonotonic Reasoning, pages 9-15. Helsinki University of Technology, 1998.

DTV99
M. Daniele, P. Traverso, and M. Vardi.
Strong Cyclic Planning Revisited.
1999.
Submitted to the 5th European Conference on Planning.

EC98
H.-D. Ehrich and C. Caleiro.
Specifying communication in distributed information systems.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1096 Lisboa, Portugal, 1998.
Submitted for publication.

Fis98
J. Fischer.
Some equation-less constructions in double categories.
Preprint 12, Fakultät für Informatik, Universität Magdeburg, 1998.

Fis99a
J. Fischer.
Concepts of object paradigm for an approach to modular specification of communication protocols.
Appears as preprint, 1999.

Fis99b
J. Fischer.
Specification of communication protocols: Extending timing diagrams for that purpose.
Appears as preprint, 1999.

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.

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.

GKW97
S. Gilmore, D. Kirli, and C. Walton.
Dynamic ML without dynamic types.
Technical Report ECS-LFCS-97-378, Laboratory for Foundations of Computer Science, Department of Computer Science, The University of Edinburgh, 1997.

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.
In Portuguese - Supervised by C. Sernadas.

GS99
P. Gouveia and C. Sernadas.
Abductive reasoning over temporal specifications of objects.
In K. Segerberg, M. Zakharyaschev, M. de Rijke, and H. Wansing, editors, Advances in Modal Logic. Volume II. CSLI Publications, 1999.
In print.

Gue99
A. S. D. L. Guerra.
Defaults in the Specification of Reactive Systems.
PhD thesis, Instituto Superior Técnico, Universidate Técnica de Lisboa, Lisbon, Portugal, January 1999.

HD99
P. Heymans and E. Dubois.
Scenario-based techniques for supporting the elaboration and the validation of formal requirements.
Requirements Engineering Journal (to appear), 1999.

HH98
P. Haumer and P. Heymans.
An integration of scenario-based requirements elicitation and validation techniques.
Technical Report CREWS-98-28, University of Namur and RWTH Aachen, 1998.

HHJP99
P. Haumer, P. Heymans, M. Jarke, and K. Pohl.
Bridging the gap between past and future in re : a scenario-based approach.
In To appear in Proc. of the Fourth IEEE International Symposium on Requirements Engineering (RE'99), Limerick, Ireland, 1999.

HLS99
Klaus Havelund, Kim G. Larsen, and Arne Skou.
Formal Verification of a Power Controller Using the Real-Time Model Checker UPPAAL.
In Joost-Pieter Katoen, editor, Proceeding of the 5th International AMAST Workshop, ARTS'99 on Formal Methods for Real-Time and Probabilistic Systems, volume 1601 of Lecture Notes in Computer Science, pages 277-298. Springer, 1999.

HRS98
Thomas A. Henzinger, Jean-Francois Raskin, and Pierre-Yves Schobbens.
The regular real-time languages.
In K. Larsen, editor, Proceedings of ICALP'98: International Colloquium on Automata, Languages and Programming, volume 1343 of Lecture Notes in Computer Science, pages 580-591, Aalborg, Denmark, July 1998. Springer-Verlag.

HS98a
Maritta Heisel and Jeanine Souquières.
Detecting feature interactions - a heuristic approach.
In G. Saake and Can Türker, editors, Proc. of the first FIREworks Workshop, Preprint 10/98, pages 30-48, Fakultät für Informatik, 1998. Univ. Magdeburg.

HS98b
Maritta Heisel and Jeanine Souquières.
A heuristic approach to detect feature interactions in requirements.
In K. Kimbler and W. Bouma, editors, Proc. 5th Feature Interaction Workshop, pages 165-171. IOS Press Amsterdam, 1998.

HS98c
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 Press, 1998.

HSC+99
M. Höding, K. Schwarz, S. Conrad, G. Saake, S. Balko, A. Diekmann, E. Hildebrandt, K.-U. Sattler, I. Schmitt, and C. Türker.
SIGMAFDB: Overview of the Magdeburg-Approach to Database Federations.
In S. Conrad, W. Hasselbring, and G. Saake, editors, Proc. 2nd Int. Workshop on Engineering Federated Information Systems, EFIS'99, Kühlungsborn, Germany, May 5-7, 1999, pages 139-146. infix-Verlag, Sankt Augustin, 1999.

HT98
J. Hillston and N. Thomas.
Product form solution for a class of PEPA models.
In Proceedings of IEEE International Computer Performance and Dependability Symposium, Durham, NC, September 1998.
To appear in a special issue of Performance Evaluation.

JMZ98
Philippe Du Bois Jean-Marc Zeippen, Eric Dubois.
Supporting the analyst when reasoning on requirements specifications for real-time and distributed systems.
In Proc. of ISORC '98 (First IEEE International Symposium on Object-Oriented Real-Time Distributed Computing), pages 215-219, Kyoto (Japan), April 1998. IEEE, Springer-Verlag.

Ki99
D. Kirli.
A static type system for detecting potentially transmissible functions.
In P. Sewell and J. Vitek, editors, Proceedings of the 5th Mobile Object Systems Workshop: Programming Languages for Wide Area Networks, Lisbon, Portugal, June 1999.

KNSS98
Marta Kwiatkowska, Gethin Norman, Roberto Segala, and Jeremy Sproston.
Verifying quantitative properties of continuous probabilistic real-time graphs.
Technical Report CSR-98-11, University of Birmingham, 1998.

KNSS99
Marta Kwiatkowska, Gethin Norman, Roberto Segala, and Jeremy Sproston.
Automatic verification of real-time systems with discrete probability distributions.
In ARTS'99: Proceedings of the 5th International AMAST Workshop on Real-Time and Probabilistic Systems, volume 1601 of Lecture Notes in Computer Science, pages 55-75. Springer-Verlag, 1999.

Lom99
Alessio Lomuscio.
Knowledge Sharing among Ideal Agents.
PhD thesis, School of Computer Science, University of Birmingham, Birmingham, UK, February 1999.

Lou
H. Lourenço.
Topic: Hybrid systems.
PhD thesis, IST, Universidade Técnica de Lisboa.
Supervised by A. Sernadas. In preparation.

LR98
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.

LR99a
A. Lomuscio and M. Ryan.
An algorithmic approach to knowledge evolution.
Artificial Intelligence for Engineering Design, Analysis and Manufacturing (AIEDAM), 13(2), 1999.

LR99b
A. R. Lomuscio and M. D. Ryan.
A spectrum of modes of knowledge sharing between agents.
In Sixth International Workshop on Agent Theories Architectures and Languages (ATAL-99. Springer-Verlag, 1999.

Mat
Paulo Mateus.
Topic: Probabilistic logic.
PhD thesis, IST, Universidade Técnica de Lisboa.
In preparation - Supervised by A. Sernadas and C. Sernadas.

McM93
K.L. McMillan.
Symbolic Model Checking.
Kluwer Academic Publ., 1993.

MGB99
F. Mercier, P. Le Gall, and A. Bertolino.
Formalizing integration test strategies for distributed systems.
In ICSE workshop on Testing Distributed Component-Based Systems, Los Angeles, 1999.

MGBB98
F. Mercier, P. Le Gall, A. Bertolino, and G. Bernot.
A systematic approach for integration testing of complex systems.
In International Conference on Software Engineering and its Applications, Paris, 1998.

MSS99
P. Mateus, A. Sernadas, and C. Sernadas.
Precategories for combining probabilistic automata.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1096 Lisboa, Portugal, 1999.
Early version presented at FIREworks Meeting, Magdeburg, May 15-16, 1998. Submitted for publication.

OCS99
H. Oakasha, S. Conrad, and G. Saake.
Consistency Management in Object-Oriented Databases.
1999.
Accepted to The 1st ECOOP Workshop on Object-Oriented Databases Lisbon - Portugal, 15 June 1999 .

OS98a
H. Oakasha and G. Saake.
Compiling State Constraints.
Technical Report 11, Fakultät für Informatik, Universität Magdeburg, 1998.

OS98b
H. Oakasha and G. Saake.
Foundations for Integrity Independence in Relational Databases.
In T. Polle, T. Ripke, and K.-D. Schewe, editors, Preproceedings 7th International Workshop on Foundations of Models and Languages for Data and Objects (FoMLaDO'98, Timmel, Oct. 1998), number 685 in Forschungsbericht, pages 142-164. Fachbereich Informatik, Universität Dortmund, 1998.

OS98c
H. Oakasha and G. Saake.
Integrity Independence in Object-Oriented Database Systems.
In M. H. Scholl, H. Riedel, T. Grust, and D. Gluche, editors, Kurzfassungen -- 10. Workshop ``Grundlagen von Datenbanken'', Konstanz (02.06.-05.06.98), number 63, pages 94-98. Universität Konstanz, Fachbereich Informatik, 1998.

OS99
H. Oakasha and G. Saake.
Foundations for Integrity Independence in Relational Databases.
In T. Polle, T. Ripke, and K.-D. Schewe, editors, Fundamentals of Information Systems, chapter 12, pages 143-165. Kluwer Academic Publishers, Boston, 1999.

Pac98
S. Pacheco.
Situation Calculus in COQ.
Technical report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1096 Lisboa, Portugal, 1998.
Diploma thesis - Supervised by A. Sernadas and J. Ramos.

Pai98
N. Paiva.
Temporal logic in COQ.
Technical report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1096 Lisboa, Portugal, 1998.
Diploma thesis - Supervised by A. Sernadas and C. Caleiro.

PR98a
M. C. Plath and M. D. Ryan.
Plug and play features.
In W. Bouma, editor, Feature Interactions in Telecommunications Systems V, pages 150-164. IOS Press, 1998.

PR98b
Malte Plath and Mark Ryan.
A feature construct for promela.
In SPIN'98 - Proceedings of the 4th SPIN workshop, November 1998.

PR99
M. C. Plath and M. D. Ryan.
Feature integration using a feature construct.
Submitted to Science of Computer Programming, 1999.

PRB+98
V. Plihon, J. Ralyte, A. Benjamen, N.A.M. Maiden, A. Sutcliffe, E. Dubois, and P. Heymans.
A reuse-oriented approach for the construction of scenario based methods.
In In Proc. of the International Software Process Association's 5th International Conference on Software Process (ICSP'98), Chicago, Illinois, USA, 1998.

PSSM99
J. Pinto, A. Sernadas, C. Sernadas, and P. Mateus.
Non-determinism and uncertainty in the situation calculus.
In Proceedings of the FLAIRS'99 - the 12th International Florida AI Research Symposium. AAAI Press, 1999.
In print.

Ram
J. Ramos.
Situation and State Calculus: Object specification, verification and reification.
PhD thesis, IST, Universidade Técnica de Lisboa.
In preparation - Supervised by A. Sernadas.

Rav
A. Ravara.
Topic: Type theory and concurrency.
PhD thesis, IST, Universidade Técnica de Lisboa.
In preparation - Supervised by V. Vasconcelos and A. Sernadas.

Res99a
P. Resende.
Modular specification of concurrent systems with observational logic.
In J.L. Fiadeiro, editor, Recent Developments in Algebraic Development Techniques, Selected Papers, volume 1589 of Lecture Notes in Computer Science, pages 307-321. Springer-Verlag, 1999.
In print.

Res99b
P. Resende.
Quantales, finite observations and strong bisimulation.
Theoretical Computer Science, 1999.
In print.

RRV98
A. Ravara, P. Resende, and V. Vasconcelos.
Towards an algebra of dynamic object types.
In ICALP'98 workshop Semantics of Objects as Processes. BRICS Note Series, 1998.

RS99
J. Ramos and A. Sernadas.
The situation and state calculus versus branching temporal logic.
In J.L. Fiadeiro, editor, Recent Developments in Algebraic Development Techniques, Selected Papers, volume 1589 of Lecture Notes in Computer Science, pages 292-306. Springer-Verlag, 1999.
In print.

RSH98
Jean-Francois Raskin, Pierre-Yves Schobbens, and Thomas A. Henzinger.
Axioms for real-time logics.
In D. Sangiorgi and R. de Simone, editors, Proceedings of CONCUR'98: 9th International Conference on Concurrency Theory, volume 1466 of Lecture Notes in Computer Science (LNCS). Springer, 1998.

Sch98
Pierre-Yves Schobbens.
Axiomatization of real-time logics.
In H.-D. Ehrich, U. Goltz, and J. Meseguer, editors, Information Systems as Reactive Systems, number 200 in Dagstuhl Seminar Bericht, Feb 1998.

SFRC99
Grégoire Sutre, Alain Finkel, Olivier Roux, and Franck Cassez.
Effective recognizability and model-checking of reactive FIFFO automata.
In 7th International Conference on Algebraic Methodology and Software Technology (AMAST'98), volume 1548 of Lecture Notes in Computer Science, pages 106-123, Amazonia, Brésil, January 1999. Springer-Verlag.

SR98
P.-Y. Schobbens and Jean-Francois Raskin.
Proving a conjecture of andreka on temporal logic.
Technical report, FUNDP and Instituto Superior Tecnico, 1998.

SR99a
Pierre-Yves Schobbens and Jean-Francois Raskin.
The logic of event clocks.
Journal of Algebra, Languages and Combinatorics, 1999.
To appear.

SR99b
Pierre-Yves Schobbens and Jean-Francois Raskin.
The logic of ``initially'' and ``next'': completeness and complexity.
Information Processing Letters, (69):221-225, 1999.

SS98
I. Schmitt and G. Saake.
Merging Inheritance Hierarchies for Database Integration.
In M. Halper, editor, Proc. of the 3rd IFCIS Int. Conf. on Cooperative Information Systems, CoopIS'98, August 20-22, 1998, New York, USA, pages 322-331, Los Alamitos, CA, 1998. IEEE Computer Society Press.

SSC98
A. Sernadas, C. Sernadas, and C. Caleiro.
Denotational semantics of object specification.
Acta Informatica, 35:729-773, 1998.

SSC99
A. Sernadas, C. Sernadas, and C. Caleiro.
Fibring of logics as a categorial construction.
Journal of Logic and Computation, 9(2):149-179, 1999.

SSCM99
A. Sernadas, C. Sernadas, C. Caleiro, and T. Mossakowski.
Categorial fibring of logics with terms and binding operators.
In M. de Rijke and D. Gabbay, editors, Frontiers of Combining Systems - FroCoS'98. Research Studies Press, 1999.
In print.

SSSS98
P.-Y. Schobbens, G. Saake, A. Sernadas, and C. Sernadas.
A two-level temporal logic for evolving specifications.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1096 Lisboa, Portugal, 1998.
Submitted for publication.

STS98
K. Schwarz, C. Türker, and G. Saake.
Execution Dependencies in Transaction Closures.
In M. Halper, editor, Proc. of the 3rd Int. Conf. on Cooperative Information Systems, CoopIS'98, August 20-22, 1998, New York City, USA, pages 122-131, Los Alamitos, CA, 1998. IEEE Computer Society Press.

TS99
C. Türker and G. Saake.
Consistent Handling of Integrity Constraints and Extensional Assertions for Schema Integration.
In Advances in Databases and Information Systems, Proc. Third East-European Symposium, ADBIS'99, Maribor, Slovenia, September 1999, Lecture Notes in Computer Science, Berlin, 1999. Springer-Verlag.
To appear.

Wal99
C. Walton.
Abstract machines for memory management.
Technical Report ECS-LFCS-99-410, Laboratory for Foundations of Computer Science, Department of Computer Science, The University of Edinburgh, June 1999.

WKG99
C. Walton, D. Kirli, and S. Gilmore.
An abstract machine model of dynamic module replacement.
Future Generation Computer Systems, 1999.
To appear in a special issue devoted to the proceedings of the Workshop on Principles of Abstract Machines held in Pisa, Italy, June 1998.

ZSS99
A. Zanardo, A. Sernadas, and C. Sernadas.
Fibring: Completeness preservation.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1096 Lisboa, Portugal, 1999.
Submitted for publication.

About this document ...

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

Copyright © 1993, 1994, 1995, 1996, 1997, Nikos Drakos, Computer Based Learning Unit, University of Leeds.

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

The translation was initiated by Malte Plath on 2000-10-18

Malte Plath
2000-10-18

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