download this bibliography
FIREworks

Feature Integration in Requirements Engineering

ESPRIT Working Group 23531


Publications

[1]
FIREworks: Technical report for year 1, May 1998. (PostScript) (DVI)

[2]
FIREworks: Technical report for year 2, June 1999. (PostScript) (DVI)

[3]
FIREworks: Technical report for year 2, December 2000. (PostScript) (DVI)

[4]
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.
In this paper, we focus on a refinement method for an object oriented algebraic formalism, called ETOILE-specifications. Étoile-specifications extend algebraic specification techniques to deal with concurrent (active) object systems. The dynamic behavior of object systems rely on implicit states used as modifiers of semantics of functionalities (or methods). Although most people affirm that objects preserve the ``good properties'' of modularity, we show that the global correctness of a system cannot be established from the local correctness of each object. This is due to the concurrency between objects. To circumvent this non modular behavior of objects, we propose a refinement theory (abstract implementation) which allows to retrieve incrementality to establish correctness. We prove that usual results concerning reuse of implementations are extended to ETOILE-specifications.

[5]
Daniel Amyot.
Use case maps as a feature description notation.
In Gilmore and Ryan [70], pages 27-44. (PostScript)

[6]
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.

[7]
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.

[8]
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.

[9]
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.

[10]
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 abridged - mcp).
In dynamic testing, a program is flagged incorrect if it fails for a test set. But how far can a successful program be considered as correct? We give a definition of program correctness with respect to a specification which is adequate to dynamic testing. Similarly to the field of abstract implementation, in order to declare a program as correct, it suffices that its behavior fulfills the specification requirements. An intermediate semantic level between the program and the specification, the oracle framework, is introduced in order to interpret observable results of dynamic experiments on the program. This allows to give algebraic semantics to the program. Program correctness is then defined by some adequacy criterion between the specification semantics and the program semantics. For some specifications, there exist exhaustive test sets (the success of which means program correctness), for some other specifications, there only exist ``complete'' (but not exhaustive) test sets.

[11]
D. Aspinall.
Type Systems for Modular Programs and Specifications.
PhD thesis, Laboratory for Foundations of Computer Science, Department of Computer Science, The University of Edinburgh, 1997.

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

[13]
G. Behrmann, K. G. Larsen, H. R. Andersen, H. Hulgaard, and J. Lind-Nielsen.
Verification of hierarchical state/event systems using reusability and compositionality.
In Proceedings of TACAS'99, volume 1579 of LNCS. Springer Verlag, 1999.

[14]
Karim Berkani, Pascale Le Gall, and Francis Klay.
An incremental method for the design of feature-oriented systems.
In Gilmore and Ryan [70], pages 45-64. (PostScript)

[15]
G. Bernot, H. Jouve, F. Klay, and J.-L. Richier F. Ouabdesselam.
Aide à l'intégration de services par la génération de tests.
In Approches formelles dans l'Assistance au developpement de Logiciel - AFADL 2000.

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

[17]
S. Béroff and M. Aiguier.
Real time algebraic specifications.
Research Report 23, Laboratoire de Mathématiques et d'Informatique, Université d'Evry-Val d'Essonne, Cours Monseigneur Roméro, Evry, France, 1997.
short english version of the TSI paper.
We introduce a notion of time into the algebraic specification framework, on the one hand for dealing with classical temporal constraints, and on the other hand to specify functions whose semantics is timely dependent. Syntax, semantics and inference system for real-time algebraic specifications are defined. A small example is also developed in order to help intuition.

[18]
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.
We introduce a notion of time into the algebraic specification framework, on the one hand for dealing with classical temporal constraints, and on the other hand to specify functions whose semantics is timely dependent. Syntax, semantics and inference system for real-time algebraic specifications are defined. A small example is also developed in order to help intuition.

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

[20]
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, January 1999.

[21]
Michel Bidoit, Donald Sannella, and Andrzej Tarlecki.
Architectural specifications in CASL.
In Proc. 7th Intl. Conference on Algebraic Methodology and Software Technology (AMAST'98), volume 1548 of Lecture Notes in Computer Science, pages 341-357. Springer, 1999. (PostScript) (PDF) (DVI)
One of the novel features of CASL, the Common Algebraic Specification Language, is the provision of so-called architectural specifications for describing the modular structure of software systems. A discussion of refinement of CASL specifications provides the setting for a presentation of the rationale behind architectural specifications. This is followed by details of the features provided in CASL for architectural specifications, hints concerning their semantics, and simple results justifying their usefulness in the development process.

[22]
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.

[23]
C. Caleiro.
Combining Logics.
PhD thesis, IST, Universidade Técnica de Lisboa, 2000.
Supervised by A. Sernadas. Awaiting examination. (DVI)

[24]
Dominique Cansell and Dominique Méry.
Abstraction and refinement of features.
In Gilmore and Ryan [70], pages 65-84. (PostScript)

[25]
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.

[26]
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.

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

[28]
Franck Cassez and Kim G. Larsen.
The impressive power of stopwatches.
In Dale Miller and Catuscia Palamidessi, editors, CONCUR '00: Concurrency Theory, 11th International Conference, volume ?? of Lecture Notes in Computer Science, Penn-State Univ., Pennsylvania, 22-25 August 2000. Springer-Verlag.

[29]
Franck Cassez, Mark Dermot Ryan, and Pierre-Yves Schobbens.
Proving feature non-interaction with Alternating-Time Temporal Logic.
In Gilmore and Ryan [70], pages 85-104. (PostScript)

[30]
Franck Cassez.
A model to describe feature integration.
submitted, April 1998.

[31]
Franck Cassez.
A semantic approach to feature integration.
First FIREworks Workshop, FIREworks'98, Magdeburg, Germany, 13-15 May 1998.

[32]
Franck Cassez.
Operators for structuring feature integration.
submitted, 1999.

[33]
A. Cesta and P.-Y. Schobbens, editors.
Proceedings of ModelAge'97: Formal Models of agents.
LNAI. Springer, 1998.
to appear.

[34]
François 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).
Requirements engineering specifications can greatly benefit from formal methods when concerned with justifying the correctness of specifications and proofs. Albert II is a formal specification language for capturing functional requirements inherent to real-time, distributed systems. Targeted to requirements engineering activities, Albert II exhibits a high expressiveness through a large range of constructs. Their interactions being however very intricate, these constructs may hamper the reasoning capabilities. Formal reasoning is nevertheless still possible because the language is grounded on a real-time core logic. We motivate our approach to the construction of a formal verification system for this core logic.

[35]
Jean-François Raskin François Chabot.
The formal semantics of Albert.
Technical report, University of Namur, Computer Science Institute, 1998.
(abstract abridged - mcp).
Albert is a specification language intended to support the eliciting of functional requirements proper to composite and distributed real-time systems. To achieve mathematical rigour Albert has been endowed with a formal semantics. Compositionality is one of our primary target. The models of the atomic components are first individually built and then composed to yield the semantic model of the full specification. We define an intermediate language, Albert-kernel, retaining all the important concepts of Albert. With this language the main concepts of Albert (agent decomposition, action, information and perception) have a direct correspondence. We provide formal semantics for Albert-kernel. An axiomatisation of the semantics in terms of set theory and timed state sequence structures could be used as a basis for semantic reasoning tools since they usually use a less expressive logic into which our formalism could be readily abstracted.

[27]
A. Cimatti, E. Giunchiglia, F. Giunchiglia, and P. Traverso.
Planning via Model Checking: A Decision Procedure for AR.
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.

[37]
A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri.
NuSmv: a re-implementation of smv.
Technical Report 9801-06, IRST, Trento, Italy, January 1998.

[38]
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.

[39]
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.

[40]
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.

[41]
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.

[42]
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.

[43]
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.
The PEPA language is supported by a suite of modelling tools which assist in the solution and analysis of PEPA models. The design and development of these tools have been influenced by a variety of factors, including the wishes of other users of the tools to use the language for purposes which were not anticipated by the tool designers. In consequence, the suite of PEPA tools has adapted to attempt to serve the needs of these users while continuing to support the language designers themselves. In this paper we report on our experiences with the PEPA tools and give some advice gained from our experiences.

[44]
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, number 1601 in LNCS, pages 211-227, Bamberg, Germany, May 1999. Springer-Verlag.

[45]
G. Clark.
Stochastic process algebra structure for insensitivity.
In Hillston [98], pages 63-82.

[46]
M. E. Coniglio, A. T. Martins, A. Sernadas, and C. Sernadas.
Fibring (para)consistent logics.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2000.
Extended abstract. Presented at II World Congress on Paraconsistency - WCP'00. (PDF)

[47]
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.

[48]
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.

[49]
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.

[50]
M. J. Coutinho.
Topic: Preservation of properties in combination of logics.
PhD thesis, IST, Universidade Técnica de Lisboa.
In preparation - Supervised by C. Sernadas.

[51]
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.

[52]
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.

[53]
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.

[54]
L. du Bousquet and N. Zuanon.
An overview of lutess, A specification-based tool for testing synchronous software.
In 14th IEEE International Conference on Automated Software Engineering. IEEE, October 1999.

[55]
L. du Bousquet, F. Ouabdesselam, J.-L. Richier, and N. Zuanon.
Incremental feature validation : a synchronous point of view.
In Feature Interactions in Telecommunications Systems V, pages 262-275. IOS Press, 1998.

[56]
L. du Bousquet, F. Ouabdesselam, J.-L. Richier, and N. Zuanon.
Lutess: a specification-driven testing environment for synchronous software.
In 21st International Conference on Software Engineering, pages 267-276. ACM Press, May 1999.

[57]
L. du Bousquet, F. Ouabdesselam, J.-L. Richier, and N. Zuanon.
Feature interaction detection using synchronous approach and testing.
Computer Networks and ISDN Systems, 32(4), April 2000.

[58]
L. du Bousquet.
Feature interaction detection using testing and model-checking, experience report.
In World Congress on Formal Methods, Toulouse, France, September 1999.

[59]
H.-D. Ehrich and C. Caleiro.
Specifying communication in distributed information systems.
Acta Informatica, 36(Fasc. 8):591-616, 2000.
We present two logics that allow specifying distributed information systems, emphasizing communication among sites. The low-level logic D0 offers features that are easy to implement but awkward to use for specification, while the high-level logic D1 offers convenient specification features that are not easy to implement. We show that D1 specifications may be automatically translated to D0 in a sound and complete way. In order to prove soundness and completeness, we define our translation as a simple map of institutions. Our result may be useful for making implementation platforms like CORBA easier accessible by providing high-level planning and specification methods for communication.

[60]
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.

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

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

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

[64]
P. Le Gall, G. Bernot, and L. Bouaziz.
A theory of probabilistic functional testing.
In Proc. of the Intl. Conf. on Software Engineering. ICSE'97, 1997.
We propose a framework for ``probabilistic functional testing.'' The success of a test data set generated according to our method guarantees a certain level of confidence into the correctness of the system under test, as a function of two parameters. One is an estimate of the reliability, and the other is an estimate of the risk that the vendor takes when (s)he notifies this reliability percentage to the client. These results are based on the theory of ``formula testing'' developed in the article. We also present a first prototype of a tool which assists test case generation according to this theory. Lastly, we illustrate our method on a small formal specification.

[65]
C. Gaston, M. Aiguier, and P. Le Gall.
Algebraic treatment of feature-oriented systems.
Technical Report 44-2000, University of Evry Val-d'Essonne - France, January 2000.

[66]
Christophe Gaston, Marc Aiguier, and Pascale Le Gall.
Algebraic treatment of feature-oriented systems.
In Gilmore and Ryan [70], pages 105-124. (PostScript)

[67]
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.
We consider the feature interaction problem in the context of the use of the PEPA stochastic process algebra.

[68]
Stephen Gilmore and Jane Hillston.
Performance modelling in PEPA with higher-order functions.
pages 35-46, 2000.

[69]
Stephen Gilmore and Jane Hillston.
The PEPA feature construct.
In Gilmore and Ryan [70], pages 125-142. (PostScript)

[70]
Stephen Gilmore and Mark Ryan, editors.
Language Constructs for Describing Features.
Springer-Verlag London Ltd, 2000/2001.

[71]
Stephen Gilmore and Mark Ryan.
Preface.
In Language Constructs for Describing Features [70], pages iii-iv. (PostScript)

[72]
S. Gilmore, J. Hillston, and M. Ribaudo.
An efficient algorithm for aggregating PEPA models.
Submitted for publication, 1998.
Performance Evaluation Process Algebra (PEPA) is a formal language for performance modelling based on process algebra. It has previously been shown that using the process algebra apparatus compact performance models can be derived which retain the essential behavioural characteristics of the modelled system. However no efficient algorithm for this derivation was given. In this paper we present an efficient algorithm which recognises and takes advantage of symmetries within the model and avoids unnecessary computation. The algorithm is illustrated by a multiprocessor example. Although it is much more efficient than the previously proposed techniques the algorithm is subject to some limitations. In particular it will not always achieve the best possible aggregation. This case is also illustrated by an example, and we discuss when this limitation is likely to have an impact on performance analysis.

[73]
S. Gilmore.
Deep type inference for mobile functions.
In P. Trinder, G. Michaelson, and H-W. Loidl, editors, Trends in Functional Programming: Proceedings of the First Scottish Functional Programming Workshop, pages 40-48. Inspect, August 2000.

[74]
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.

[75]
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.

[76]
The CoFI Semantics Group.
CASL - the CoFI algebraic specification language (version 0.97) - semantics.
CoFI Note, 1997.

[77]
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.

[78]
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.

[79]
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.

[80]
S. Guerra.
Defaults in specifications: distance functions between temporal models.
In I. Kruijff-Korbayov a, editor, Proceedings of the Third ESSLII Student Session, 1998.

[81]
S. Guerra.
Defaults in the Specification of Reactive Systems.
PhD thesis, IST, Universidade Técnica de Lisboa, 1999.
Supervised by M. Ryan and A. Sernadas.

[82]
J. Hannay.
Relative equational specification and semantics.
Technical Report ECS-LFCS-97-366, Laboratory for Foundations of Computer Science, Department of Computer Science, The University of Edinburgh, 1997.

[83]
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.

[84]
K. Havelund, K. G. Larsen, K. Lund, and A. Skou.
Formal modelling and analysis of an audio/video protocol: An industrial case study using UPPAAL.
In In Proc. of the 18th IEEE Real-Time Systems Symposium. IEEE, 1997.

[85]
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.

[86]
K. Havelund, K. G. Larsen, and A. Skou.
Formal verification of a power controller using the real-time model checker UPPAAL.
In Joost-Pieter Katoen, editor, Proceedings of the 5th International AMAST Workshop, 1999.

[87]
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.

[88]
Maritta Heisel and Jeanine Souquières.
Detecting Feature Interaction - A Heuristic Approach.
In G. Saake and C. Turker, editors, 1st FIREworks Workshop, Magdeburg, Germany, May 1998.

[89]
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.

[90]
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, September 1998.

[91]
Maritta Heisel and Jeanine Souquières.
Methodological support for requirements elicitation and formal specification.
In Proc. 9th International Workshop on Software Specification and Design - WSSD'98, Kyoto, Japan, pages 153-155. IEEE Computer Society Press, April 1998.

[92]
Maritta Heisel and Jeanine Souquières.
A Method for Requirements Elicitation and Formal Specification.
In ER'99 (18th International Conference on Conceptual Modeling), Paris, volume 1728 of LNCS, pages 309-324, November 1999.

[93]
Maritta Heisel and Jeanine Souquières.
De l'élicitation des besoins à la spécification formelle.
Technique et Science Informatiques, 18(7):777-801, September 1999.

[94]
Maritta Heisel and Jeanine Souquières.
Requirements Elicitation for a Light Control System.
In Seminar No. 99241, Schloss Dagstuhl, Requirements Capture, Documentation and Validation, Dagstuhl, Wadern, Germany. E. Börger (Universita di Pisa, I), B. Hörger (Daimler-Benz, Ulm, D), D. Parnas (McMaster University, CAN), D. Rombach (Universitšt Kaiserslautern, D), June 1999.

[95]
Maritta Heisel and Jeanine Souquières.
A heuristic algorithm to detect feature interactions in requirements.
In Gilmore and Ryan [70], pages 143-162. (PostScript)

[96]
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.
A specification formalism for real-time systems defines a class of timed omega -languages, whose letters have real-numbered time stamps. Two popular ways of specifying timing constraints rely on the use of clocks, and on the use of time bounds for temporal operators. However, temporal logics with clocks or time bounds have undecidable satisfiability problems, and finite automata with clocks (so-called timed automata) are not closed under complement. Therefore, two fully decidable restrictions of these formalisms have been proposed. In the first case, clocks are restricted to event clocks, which measure distances to immediately preceding or succeeding events only. In the second case, time bounds are restricted to nonsingular intervals, which cannot specify the exact punctuality of events. We show that the resulting classes of timed omega -languages are robust, and we explain their relationship.

[97]
J. Hillston and L. Kloul.
Performance evaluation of an on-line auction system.
Concurrency: Practice and Experience, 2000.
To appear.

[98]
J. Hillston, editor.
Proceedings of the Seventh Annual Workshop on Process Algebra and Performance Modelling, Zaragosa, Spain, September 1999. University of Zaragosa Press.

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

[100]
Furio Honsell, John Longley, Donald Sannella, and Andrzej Tarlecki.
Constructive data refinement in typed lambda calculus.
In Proc. 3rd Intl. Conf. on Foundations of Software Science and Computation Structures. European Joint Conferences on Theory and Practice of Software (ETAPS'2000), volume 1784 of Lecture Notes in Computer Science, pages 149-164. Springer, 2000. (PostScript) (PDF) (DVI)
A new treatment of data refinement in typed lambda calculus is proposed, phrased in terms of pre-logical relations [HS99] rather than logical relations, and incorporating a constructive element. Constructive data refinement is shown to have desirable properties, and a substantial example of refinement is presented.

[101]
T. Iversen, K. Kristoffersen, K. G. Larsen, M. Laursen, R. G. Madesen, S. K. Mortensen, P. Pettersson, et al.
Model-checking real-time control programs.
submitted, 1999.

[102]
Stefan Kahrs and Donald Sannella.
Reflections on the design of a specification language.
In Proc. Intl. Colloq. on Fundamental Approaches to Software Engineering. European Joint Conferences on Theory and Practice of Software (ETAPS'98), volume 1382 of Lecture Notes in Computer Science. Springer, 1998. (PostScript) (PDF) (DVI)
We reflect on our experiences from work on the design and semantic underpinnings of Extended ML, a specification language which supports the specification and formal development of Standard ML programs. Our aim is to isolate problems and issues that are intrinsic to the general enterprise of designing a specification language for use with a given programming language. Consequently the lessons learned go far beyond our original aim of designing a specification language for ML.

[103]
F. Laroussinie and K. G. Larsen.
CMC: A tool for compositional model checking of real-time systems.
In Proceedings of FORTE/PSTV Conference, Paris 1998, November 1998.

[104]
J. Loeckx, H.-D. Ehrich, and M. Wolf.
Algebraic specification of abstract data types.
In S. Abramski, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Theoretical Computer Science, Volume 5. Oxford University Press, 2000.
To appear.

[105]
H. Louren c co and A. Sernadas.
Combining hybrid systems.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 1999.

[106]
H. Louren c co and A. Sernadas.
An institution of hybrid systems.
In Didier Bert and Christine Choppy, editors, Recent Developments in Algebraic Development Techniques - Selected Papers, volume 1827 of Lecture Notes in Computer Science, pages 219-236. Springer-Verlag, 2000.

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

[108]
H. Lourenço, 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.

[109]
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.
Due to practical limitations in software and hardware, data type implementations are always bounded. Such limitations are a frequent source of faults which are difficult to find out. As soon as boundaries are clearly identified in a specification, functional testing should be able to address any boundary fault. We propose to enrich a data type specification formalism, namely algebraic specifications, allowing a natural description of data type boundaries. This enhancement allows us to adapt the existing testing theory, the method and the tool, initially dedicated to functional testing from unbounded data type specifications. Several examples of test data selection with the LOFT tool, from two bounded data type specifications will illustrate the benefit of our approach: an assisted test selection process, formally defined in a functional testing theory, allowing adequate coverage of both data types bounds and the definition domains of the specified operations.

[110]
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.

[111]
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.

[112]
P. Mateus, A. Sernadas, and C. Sernadas.
Precategories for combining probabilistic automata.
Electronic Notes in Theoretical Computer Science, 29, 1999.
Early version presented at FIREworks Meeting, Magdeburg, May 15-16, 1998. Presented at CTCS'99, Edinburgh, September 10-12, 1999.

[113]
P. Mateus, M. Cabral Morais, C. Nunes, A. Pacheco, A. Sernadas, and C. Sernadas.
Randomly timed automata.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, March 2000.
Submitted for publication. (PDF)

[114]
P. Mateus, A. Pacheco, J. Pinto, A. Sernadas, and C. Sernadas.
Probabilistic situation calculus.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, March 2000.
Submitted for publication. (PDF)

[115]
P. Mateus, A. Sernadas, and C. Sernadas.
Realization of probabilistic automata: Categorical approach.
In Didier Bert and Christine Choppy, editors, Recent Developments in Algebraic Development Techniques - Selected Papers, volume 1827 of Lecture Notes in Computer Science, pages 237-251. Springer-Verlag, 2000. (PDF)

[116]
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.

[117]
P. Mateus.
Interconnection of Probabilistic Systems.
PhD thesis, IST, Universidade Técnica de Lisboa, 2000.
Supervised by A. Sernadas and C. Sernadas. Awaiting examination. (DVI)

[118]
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.

[119]
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.

[120]
U. Nestmann and A. Ravara.
What's tyCO, after all?
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2000.
Short abstract. Presented at Express'00, satellite event of CONCUR'00.

[121]
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.

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

[123]
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.

[124]
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.

[125]
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.

[126]
H. Oakasha, S. Conrad, and G. Saake.
Consistency Management in Object-Oriented Databases.
In A. de Miguel, E. Ferrari, G. Kappel, G. Guerrini, and I. Merlo, editors, Proc. of the 1st ECOOP'99 Workshop on Object-Oriented Databases (Lisbon, Portugal, June 15th, 1999), pages 97-108, 1999.

[127]
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.

[128]
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.

[129]
J. Pinto, A. Sernadas, C. Sernadas, and P. Mateus.
Non-determinism and uncertainty in the Situation Calculus.
In A. Kumar and I. Russell, editors, Proceedings of the FLAIRS'99 - the 12th International Florida AI Research Symposium, pages 454-460. AAAI Press, 1999.
Short version of [130].

[130]
J. Pinto, A. Sernadas, C. Sernadas, and P. Mateus.
Non-determinism and uncertainty in the Situation Calculus.
International Journal of Uncertainty, Fuzziness and Knowledge-Based Systems, 8(2):127-149, 2000.
Full version of [129].

[131]
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.
We propose a feature construct for defining features, and use it to provide a plug-and-play framework for exploring feature interactions. Our approach to the feature interaction problem has the following characteristics: (a) features are treated as first-class objects during the development phase; (b) a method for integrating a feature into a system description is described. It allows features to override existing behaviour of the system being developed; (c) a prototype tool has been developed for performing the integration; (d) our approach allows interactions between features to be witnessed. In principle, our approach is quite general and need not be tied to any particular system description language. In this paper, however, we develop the approach in the context of the SMV model checking system. We describe two case studies in detail: the lift system, and the telephone system.

[132]
Malte Plath and Mark Ryan.
A feature construct for promela.
In SPIN'98 - Proceedings of the 4th SPIN workshop, November 1998.
A feature is an increment of functionality that can be added to an existing system. Many features override the default behaviour of the system, and can lead to unexpected situations. Adding several features to a system is very likely to introduce inconsistencies among their functionality, even if each feature works correctly in isolation. To facilitate the development of features and the detection of inconsistencies between features, using model checking, we extend Promela with a Feature Construct. This construct allows us to define changes to a given Promela program in a clearly structured and intuitive way. The features thus defined are then automatically integrated into the Promela description of the base system by means of a preprocessor. The developer need not (and should not) alter the original code except through the feature integration process.

[133]
M. C. Plath and M. D. Ryan.
Feature integration using a feature construct.
To appear in Science of Computer Programming, Elsevier Publishing, 1999.

[134]
M. C. Plath and M. D. Ryan.
SFI: a feature integration tool.
Advances in Computer Science, pages 201-216, 1999.

[135]
M. C. Plath and M. D. Ryan.
Entry for FIW'00 Feature Interaction Contest.
Technical report, School of Computer Science, University of Birmingham, February 2000.
Available from url ftp://ftp.cs.bham.ac.uk/pub/authors/M.D.Ryan/00-fiw-contest.ps.gz.

[136]
Malte Plath and Mark Dermot Ryan.
Defining features for CSP: Reflections on the feature interaction contest.
In Gilmore and Ryan [70], pages 163-176. (PostScript)

[137]
Malte C. Plath.
Language Constructs for Defining Features for Reactive Systems.
PhD thesis, School of Computer Science, The University of Birmingham, School of Computer Science, The University of Birmingham, Edgbaston, Birmingham, B15 2TT, United Kingdom, October 2000.
submitted Oct 2000. (PostScript)
Feature-oriented specification addresses the problem of how to add new functionality to a system in a systematic way. A feature is a unit of functionality that can be added to an existing system. Sometimes however, combinations of features produce unexpected results. This phenomenon has become known as feature interaction. Features and feature interactions can be found in any system that is enhanced with new or optional functionality. Feature-oriented specification addresses three central questions: begin itemize item how to specify features for a system, item how to add features to the system, and item how to detect interactions among features. end itemize The method proposed here is to extend specification languages with constructs for defining features, so-called feature constructs. Each feature construct is complemented by a notion of feature integration: a method for adding a feature definition to the specification of a system. Feature integration gives semantics to a feature construct. This thesis details feature constructs for three specification languages, SMV , Promela and CSP , and demonstrates their use in examples and case studies. For SMV and CSP , formal semantics of the feature constructs are developed, too. All three languages investigated are model checking languages, and we investigate the use of model checking to detect feature interactions.

[138]
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.

[139]
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.

[140]
J. Ramos.
The Situation and State Calculus: Specification and Verification.
PhD thesis, IST, Universidade Técnica de Lisboa, 2000.
Supervised by A. Sernadas. (DVI)

[141]
J. Rasga, A. Sernadas, C. Sernadas, and L. Viganò.
Fibring labelled deduction systems.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, May 2000.
Submitted for publication. (PDF)

[142]
Jean-Francois Raskin and Pierre-Yves Schobbens.
Real-time logics: Fictitious clock as an abstraction of dense time.
In Proc. Third International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS97), Lecture Notes in Computer Science (LNCS). Springer, 1997.
In this paper we study two possible semantics for the real-time logic MTL (Metric Temporal Logic). In the first semantics, called dense time semantics, time is modeled by the positive real numbers. In the second one, called fictitious clock semantics, real-time information is delivered by a global fictitious clock. We show that the fictitious clock semantics can be viewed as an abstraction of the dense time semantics. This abstraction relation is formalized by a parametric conservative connection. This formalization can be used to partially decide undecidable problems in the dense time semantics by reasoning on the fictitious clock semantics.

[143]
Jean-Francois Raskin and Pierre-Yves Schobbens.
State clock logic : a decidable real-time logic.
In Proc. International Workshop on Real-time and Hybrid Systems (HART'97), Lecture Notes in Computer Science (LNCS). Springer, 1997.
In this paper we define a real-time logic called SC logic. This logic is defined in the framework of State Clock automata, the state variant of the Event Clock automata of Alur et al. Unlike timed automata, they are complementable and thus language inclusion becomes decidable. SC automata and SC logic are less expressive than timed automata and MITL but seem expressive enough in practice. A procedure to translate each SC formula into a SC automaton is presented. The main contribution of this paper is to complete the framework of this class of determinizable automata with a temporal logic and to introduce the notion of event clock in the domain of temporal logic.

[144]
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.
This paper presents a complete axiomatization of fully decidable propositional real-time linear temporal logics with past: the Event Clock Logic ( ECL ) and the Metric Interval Temporal Logic with past ( MITL ). The completeness proof consists of an effective proof building procedure for ECL . From this result we obtain a complete axiomatization of MITL by providing axioms that allows the translation of MITL formulae into ECL formulae, the two logics being equally expressive. Our proof is structured to yield a similar axiomatization and procedure for interesting fragments of this logic: the linear temporal logic of the real numbers ( LTR ), the fragment with only past clocks.

[145]
A. Ravara and L. Lopes.
Programming and implementation issues in non-unifom tyCO.
Technical report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 1999.
Presented at OOSDS'99 (Satellite Event of ICFP'99), Paris.

[146]
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.

[147]
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.

[148]
A. Ravara and V. Vasconcelos.
Typing non-uniform concurrent objects.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2000.
Extended version of [amar:vv:00a].

[149]
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.

[150]
A. Ravara, P. Resende, and V. Vasconcelos.
An algebra of behavioural types.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 1999.
Submitted for publication.

[151]
A. Ravara.
Typing Non-uniform Concurrent Objects.
PhD thesis, IST, Universidade Técnica de Lisboa, 2000.
Supervised by V. Vasconcelos and A. Sernadas. Awaiting examination. (DVI)

[152]
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. (DVI)

[153]
P. Resende.
Quantales, concurrent observations and event structures.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 1999.
Submitted for publication.

[154]
P. Resende.
Quantales, finite observations and strong bisimulation.
Theoretical Computer Science, 1999.
In print. (DVI)

[155]
P. Resende.
Quantales and observational semantics.
In B. Coecke, D. Moore, and A. Wilce, editors, Current Research in Operational Quantum Logic: Algebras, Categories and Languages, volume 111 of Fundamental Theories of Physics, pages 263-288. Kluwer Academic Publishers, 2000.
Invited paper. (PDF) (DVI)

[156]
C. Russo.
Types for Modules.
PhD thesis, Laboratory for Foundations of Computer Science, Department of Computer Science, The University of Edinburgh, 1997.

[157]
M. Ryan and P.-Y. Schobbens.
Counterfactuals and updates.
Journal of Logic, Language and Information, 1997.
This paper summarises and systematizes the link between Counterfactual and Updates.

[158]
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.

[159]
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.

[160]
G. Saake, C. Türker, and S. Conrad.
Evolving Objects: Conceptual Description of Adaptive Information Systems.
In H. Balster, B. de Brock, and S. Conrad, editors, Int. Workshop Database Schema Evolution and Meta Modeling DEMM'2000 (9th Int. Workshop on Foundations of Models and Languages for Data and Objects), 18.-21. September 2000, Schlo\3 Dagstuhl, Germany. Participants' Proceedings, University of Twente, 2000.
(revised version to appear in Post Proceedings, LNCS, Springer-Verlag).

[161]
D. Samborski.
Stack service model.
In Gilmore and Ryan [70], pages 177-196. (PostScript)

[162]
Donald Sannella and Andrzej Tarlecki.
Algebraic methods for specification and formal development of programs.
ACM Computing Surveys, 31(3es), 1999. (PostScript) (PDF) (DVI)

[163]
Donald Sannella.
Algebraic specification and program development by stepwise refinement.
In Proc. 9th Intl. Workshop on Logic-based Program Synthesis and Transformation, LOPSTR'99, volume 1817 of Lecture Notes in Computer Science, pages 1-9. Springer, 2000. (PostScript) (PDF) (DVI)
Various formalizations of the concept of ``refinement step'' as used in the formal development of programs from algebraic specifications are presented and compared.

[164]
Donald Sannella.
The Common Framework Initiative for algebraic specification and development of software.
In Proc. 3rd Intl. Conf. on Perspectives of System Informatics (PSI'99), volume 1755 of Lecture Notes in Computer Science, pages 1-9. Springer, 2000. (PostScript) (PDF) (DVI)
The Common Framework Initiative (CoFI) is an open international collaboration which aims to provide a common framework for algebraic specification and development of software. The central element of the Common Framework is a specification language called CASL for formal specification of functional requirements and modular software design which subsumes many previous algebraic specification languages. This paper is a brief summary of past and present work on CoFI.

[165]
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.

[166]
P.-Y. Schobbens and Jean-Francois Raskin.
Proving a conjecture of Andreka on temporal logic.
Technical report, FUNDP and Instituto Superior Tecnico, 1988.
In [Andreka], a large number of completeness results about variants of discrete linear-time temporal logic are obtained. One of them is left as an open problem: the completeness of the logic of initially and next, for which a deductive system is proposed. This simple logic is of practical importance, since the proof of program invariants only require these modalities. We show here that the conjectured completeness of this system indeed holds; further, we show that the corresponding decision problem is NP-complete.

[167]
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.
Traditional information system specifications are fixed: the rules of the system are frozen at specification time. In practice, most systems have to change their rules in unexpected ways during their lifetime: business rules evolve with market pressures, the legal constraints are modified. We present here a simplified and more classical variant of a temporal logic that deals with specification evolution. It is a linear time temporal logic with two levels of time: intervals, interrupted by mutations (changes of rules), which compose lifes of the system.

[168]
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. (DVI)

[169]
L. Schröder and P. Mateus.
Universal aspects of probabilistic automata.
Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 1999.
Submitted for publication.

[170]
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.

[171]
A. Sernadas, C. Sernadas, and C. Caleiro.
Synchronization of logics.
Studia Logica, 59(2):217-247, 1997.

[172]
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.

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

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

[175]
A. Sernadas, C. Sernadas, C. Caleiro, and T. Mossakowski.
Categorial fibring of logics with terms and binding operators.
In D. Gabbay and M. de Rijke, editors, Frontiers of Combining Systems 2, pages 295-316. Research Studies Press, 2000.

[176]
Jeanine Souquières and Maritta Heisel.
Une méthode pour l'élicitation des besoins : application au système de contr^ole d'accès.
In Grenoble IMAG, editor, AFADL'2000 (Approches Formelles dans l'Assistance au Développement des Logiciels), Grenoble. Y. Ledru, président (LSR/IMAG, Grenoble), January 2000.

[177]
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.

[178]
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.
The advantages of using stochastic process algebra to specify performance models are well-documented. There remains, however, a reluctance in some quarters to use process algebras; this is particularly the case amongst queueing theorists. This paper demonstrates the use of a Markovian process algebra to represent a wide range of queueing models. Moreover, it shows that the most common interactive behaviours found in queueing systems can be modelled simply in a Markovian process algebra, and discusses how such specifications can lead to an automated numerical solution method. An additional objective of this work is to specify queueing models in a form which facilitates efficient solution techniques. It is intended that characterising the syntactic forms within the Markovian process algebra which give rise to these efficient solution methods will subsequently allow the methods to be applied to a much wider range of models specified in the process algebra.

[179]
N. Thomas, S. Gilmore, and J. Hillston.
Applying quasi-separability to Markovian process algebra.
Submitted for publication, September 1998.
Stochastic process algebras have become an accepted part of performance modelling over recent years. Because of the advantages of compositionality and flexibility they are increasingly being used to model larger and more complex systems. Therefore tools which support the evaluation of models expressed using stochastic process algebra must be able to utilise the full range of decomposition and solution techniques available. In this paper we study a class of models which do not give rise to a product form solution but can nevertheless be decomposed into their components without loss of generality. We also exemplify the use of the Markovian process algebra PEPA with the spectral expansion technique which enables a class of PEPA models with infinite state space to be solved numerically.

[180]
J. Tomasik and J. Hillston.
Transforming PEPA models to obtain product form bounds.
Technical Report EDI-INF-RR-0009, Laboratory for Foundations of Computer Science, The University of Edinburgh, February 2000.

[181]
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.

[182]
Kenneth J. Turner.
Structuring telecommunications features.
In Gilmore and Ryan [70], pages 1-10. (PostScript)

[183]
V. Vasconcelos and A. Ravara.
Comunication errors in the pi-calculus are undecidable.
Information Processing Letters, 71:229-233, 1999.

[184]
FIREworks working visit.
Talks about FIFFO, timed and hybrid automata, 1999.
IRCyN, Nantes, France, March 30 - April 1st.

[185]
T. Yoneda and T. Ohta.
The declarative language STR (State Transition Rule).
In Gilmore and Ryan [70], pages 197-212. (PostScript)

[186]
A. Zanardo, A. Sernadas, and C. Sernadas.
Fibring: Completeness preservation.
Journal of Symbolic Logic, in print. (PDF)

[187]
Pamela Zave.
Feature-oriented description, formal methods, and DFC.
In Gilmore and Ryan [70], pages 11-26. (PostScript)

[188]
Nicolas Zuanon.
Modular feature integration and validation in a synchronous context.
In Gilmore and Ryan [70], pages 213-231. (PostScript)


Generated using bib2html by David Hull (hull@cs.uiuc.edu)
command line: bib2html -a -s plain fireworks.bib publications.html


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