Final Report of the COST-247 Action

The present Web page lists all scientific presentations given during the COST 247 project.

A PDF version and a Postscript version of this document are available on the VASY ftp server.

This Page was prepared by Mark Jorgensen and Hubert Garavel.

Table of Contents

• A Survey of Value Passing Process Algebras
  Matthew Hennessy

• A Timed Full LOTOS with Time/Action Tree Semantics
  Tommaso Bolognesi

• A Formal Definition of Time in LOTOS
  Luc Leonard

• A Timed LOTOS Extension
  Juan Quemada

• A failures semantics for timed LOTOS
  Steve Schneider

• A Timed Process Algebra for Specifying Real-Time Systems
  Sergio Yovine

• The Tick-Tock Case Study for the Assessment of Timed Formal Description Techniques
  L. Léonard, G. Leduc, A. Danthine

• Case-studies using Timed Full LOTOS
  Tommaso Bolognesi

• Examples of the Use of ET-LOTOS
  Luc Leonard

• Case-studies using T-LOTOS
  Juan Quemada

• Case studies using TCSP
  Jim Davies

• Kronos: A Tool for Verifying Real-time Systems
  Sergio Yovine

• Introducing Mobility in LOTOS
  Elie Najm

• Thoughts on the future of algebraic types in LOTOS
  Muffy Thomas

• A LOTOS Verification Case Study
  Muffy Thomas

• CONCUR2: Datatypes and processes task
  Alan Jeffrey

• Reachable state space analysis of LOTOS specifications
  Alain Kerbrat

• Computable data types for E-LOTOS
  Charles Pecheur

• Overview of the CAESAR.ADT abstract data type compiler
  Hubert Garavel

• About partial functions
  Jean-Michel Hufflen

• Convenient notations everywhere with Rich Term Syntax
  Charles Pecheur

• The algebraic specification language LPG: presentation and assessment of the design choices
  Didier Bert

• The GLIDER language
  Jean-Michel Hufflen

• Overview of the SALSA project
  Didier Bert

• A monadic language for concurrent programming
  Alan Jeffrey

• Verification of a railway safety box
  Jan Friso Groote

• Developments in the definition and verification of the Xpress Transfer Protocol (XTP)
  Octavian Catrina

• Verifying mutual exclusion algorithms by reducing state spaces
  Martti Tienari

• The MEIJE verification toolset: new tools, and pragmatics
  Eric Madelaine

• Specification of the XTP Context Management Closing Procedure with a TLA
  Tatjana Kapus, Zmago Brezocnik

• A caching protocol and the Philips Xaccess bus protocol
  Susanne Graf

• The TIS approach to performance enhancements of LOTOS
  A. Wolisz

• Semantics of time constraints in concurrent systems
  P. Dembinski

• Performance measures of Estelle specifications
  M. Hendaz

• Simulation of TIS specifications with practical examples
  A. Wolisz

• Enhancement to LOTOS, status and progression of work
  Juan Quemada

• LotoTis and its Semantics
  Ina Schieferdecker

• Richer Gates for Extended LOTOS
  Jose A. Manas

• A Unified Semantical Model for Integration of LOTOS Process and TM Database Specifications, Based on Labelled Transition Systems
  Jan J. Vis

• Using Functional Data Types in Extended Algebraic Specifications: An Experience Report
  Diego Friedel

• Data Typing for Extended LOTOS
  Jose A. Manas

• Modules for Extended LOTOS
  Jose A. Manas

• The Belgian-Spanish ISO Proposal for a Timed LOTOS
  Luc Leonard

• On the Algebraic Study of ET-LOTOS
  Abdelkader Dekdouk

• Timed Modal Specifications: An Extension of CCS with Time and Refinement
  Kim Guldstrand Larsen

• Formal Specification and Generation of Use Cases for a Mobile Telephony Standard
  Luigi Logrippo, Amine Rachdi, Randy Tuok

• Approaches for Detecting Feature Interactions
  Luigi Logrippo, Mohammed Faci, and Bernard Stepien

• The Modeling and Analysis of Frame Synchronized Ring with Predicate/Transition Nets
  Tino Pyssysalo

• Verification of the XTP Closing Procedure using a TLA
  Tatjana Kapus, Zmago Brezocnik

• Experience with five industrial case studies (Philips1,2,3, NS, Ned.Haarlem, PhilipsH)
  Jan Friso Groote

• Design and use of Estelle/SDL enhanced simulators for performance predictions of a prototype XTP protocol implementation
  Stanislas Budkowski

• Simulating Extended Algebraic Specifications with SES Workbench: the SIMTIS Approach
  Jean-Pierre Ebert and Morten Schlaeger

• An implementation of SDL 92 synchronization semantics
  Vladimir Levin, Husnu Yenigun and Kemal Inan

• Open Distributed Processing: new challenges for Formal Methods
  Maarten Steen, Eerke Boiten, Howard Bowman and John Derrick

• Transformation of ET-LOTOS Processes in Extended Timed Automata
  Christian Hernalsteen

• A refinement technique in SDL design of a telephone exchange
  Eleonora Bounimova, Vladimir Levin, Kemal Inan

• Insyde - An Integrated methodology for Hybrid System Design
  Eckhardt Holz

• phi-SDL as the core of SDL with a tractable semantics
  Kees Middelburg

• Features of a new process algebra
  Kemal Inan

• Specification Architecture in a Communications Context
  Kenneth J. Turner

• Focus Points and Convergent Process Operators
  Jan Friso Groote

• An overview of the LOTOSPHERE proposal for modules in E-LOTOS
  Hubert Garavel and Mihaela Sighireanu

• Formal specification and implementation of an SDL to COSPAN compiler
  Kemal Inan

• A first experiment with ET-LOTOS: The specification of real-time schedulers
  Christian Hernalsteen

• Reduction Method for Transition System of a Performance Evaluation Extension of LOTOS
  Z. Huzar and J. Magott

• Conformance test results in Hungary
  Endre Blum and Cs.Elekes and Andras Bolcskei

• Certification in Hungary
  Janos Miskolczi and Kati Tarnay

• Derivation of protocols for specific users of distributed systems
  Marjeta Pucko and Monika Kapus-Kolar

• Specification of abstract test suites in MSC
  Maria Toeroe

• Specification in LOTOS and verification of a distributed election algorithm
  Hubert Garavel and Laurent Mounier

• A process-algebraic approach to compute and represent the global events of a LOTOS specification preserving parallelism
  David Larrabeiti Lopez

• State Exploration in TE-LOTOS with Time Extended LOLA
  Gualberto Rabay Filho

• Hardware Implementation of LOTOS specifications
  Tomas de Miguel, Tomas Robles Valladares

• EMPA : A Stochastic Process Algebra
  Marco Bernardo

• Implementation relations for Transition System Specifications
  Jan Tretmans

• An overview of the EUCALYPTUS project
  Hubert Garavel

• SPEC: SDL Performance Evaluation Tool
  Stan Budkowski

• Performance Estimations based on an XTP Formal Specification
  Piotr Dembinski

• Specification and Implementation of Components of a Toolbox for muCRL
  Jan Friso Groote

• Optimal Checking Sequence Construction Under Differing Set of Assumptions Exploiting Overlapping Constraints
  Kemal Inan

• A compositional verification tool
  Fredrik Orava

• Commercial Verification
  Robert Kurshan

• SOFTWARE/HARDWARE CO-DESIGN USING THE TWO SPECIFICATION LANGUAGES: SDL AND S/R
  Ella Bounimova

• OBJECT ORIENTED MODELLING OF ADVANCED IN SERVICES WITH SDL-92
  Ferdinando Lucidi, Alessandro Tosti, Sebastiano Trigila

• EXPERIENCE OF USING SDL IN ISKRATEL
  Ana Robnik

• SPECIFYING AND VERIFYING THE ALTERNATING BIT PROTOCOL WITH PROBABILISTIC-TIMED LOTOS
  Carlos Gregorio-Rodriguez and Manuel Nunez

• AN EXPERIMENT IN FORMALISING AND ANALYSING RAILYARD CONFIGURATIONS
  Lars-ake Fredlund and Fredrik Orava

• Functionality decomposition of basic Lotos expressions with generalized termination, enabling and disabling
  Monika Kapus-Kolar

• Demonstration of the CAESAR/ALDEBARAN toolbox
  Hubert Garavel

• TE-LOLA: A TIME EXTENDED LOLA PROTOTYPE
  David Larrabeit, Gualberto Rabay Filho

• FORMAL DESCRIPTION AND ANALYSIS OF A BOUNDED RETRANSMISSION PROTOCOL
  Radu Mateescu

• MODELLING AND VERIFYING A BOUNDED RETRANSMISSION PROTOCOL USING UPPAAL
  Pedro R. D'Argenio, Joost-Pieter Katoen, Theo Ruys, and Jan Tretmans

• ANALYSIS OF COMMUNICATION PROTOCOLS USING A THEORY OF LOSSY CHANNEL SYSTEMS
  Parosh Aziz Abdulla

• ABRUPTLY-TERMINATED CONNECTIONS IN TCP -- A VERIFICATION EXAMPLE
  Ina Schieferdecker

• EFFICIENT SYMBOLIC TRAVERSAL ALGORITHMS USING PARTITIONED TRANSITION RELATIONS
  Zmago Brezocnik, Ales Casar, Tatjana Kapus

• VERIFICATION OF SIGNALLING PROTOCOLS FOR TELECOMMUNICATION SERVICES IN INTELLIGENT NETWORK
  Bruno Blaskovic, Ignac Lovrek

• TESTING THEORY IN PRACTICE: A SIMPLE EXPERIMENT
  Rinke Terpstra, Luis Ferreira Pires, Lex Heerink, and Jan Tretmans

• TESTING OF ISDN SERVICES BASED ON SDL SPECIFICATIONS
  Marjeta Pucko

• TEST SEQUENCE GENERATION BASED ON STOCHASTICS PROGRAMMING
  P. Benczur (1), Geza Nemeth (2), Katalin Tarnay (2)

• A FUZZY MODEL FOR TEST RESULTS CERTIFICATION
  Mihaly Bohus (1), Laszlo Koczy (2), Katalin Tarnay (3)

• FORMAL DESCRIPTION ON THE TEST DOCUMENT HIERARCHY
  Ana Maria Ponce (1), Geza Nemeth (2), Janos Miskolczi (2), Katalin Tarnay (2)

• TESTING X.400
  Sarolta Dibuz

• VALIDATION OF COMMUNICATIONS PROTOCOLS
  Gyula Csopaki

• MHS MESSAGE WITH EDIM
  Gabor Borsodi (1), Sarolta Dibuz (2), Katalin Tarnay (3)

• An operational characterisation of may- and must-test in ET-LOTOS
  Luc Leonard

• Complexity of Estelle specifications
  Jean-Luc Raffy

• State Space Reduction of SDL with Partial-Order Methods
  Alper Sen

• A verification of a distributed summing protocol
  Jan Friso Groote

• Specification and Verification of the PowerScale(TM) Bus Arbitration Protocol: An Industrial Experiment with LOTOS
  Gh. Chehaibar, H. Garavel, L. Mounier, N. Tawbi, F. Zulian

• About compositional verification of TLA protocol specifications using projections
  Tatjana Kapus, Zmago Brezocnik

• Using CSP for authentication protocol analysis: the Needham-Schroeder Public Key Protocol
  Steve Schneider

• Extended Markovian Bisimulation Equivalence
  Marco Bernardo

• Animation of real-time ET-LOTOS specifications
  Christian Hernalsteen and Antony De Jacquier

• Refinement of Lotos specifications
  Timo Karvi

• Experiences with practical protocol testing
  Krzysztof M. Brzezinski, Marek Sredniawa

• Software Development in Telecommunications - Problems and Challenges
  Kristian Toivo, Antun Caric

• A Tool Framework for Verifying Concurrent Systems
  Rance Cleaveland, Steve Sims

• Verification using Leap Automata
  H. Yenigun, K. Inan

• A Practical Approach to Testing Finite State Systems
  D. Larrabeiti, J. Quemada, S. Pavon

• New Features, Applications and Perspectives for the CADP'97 Toolbox
  Hubert Garavel, M. Jorgensen, R. Mateescu, Ch. Pecheur, M. Sighireanu, B. Vivien

• Message Sequence Chart Specification and Verification using Promela/Spin
  I. Lovrek, D. Jelavic, M. Pavelic, E. Dautovic, E. Filipovic, K. Madunovic

• Software Tools for Technology Transfer
  Bernhard Steffen

• Description and Formal Specification of the Link Layer of P1394
  Bas Luttik

• Validation of the Link Layer Protocol of the IEEE-1394 Serial Bus (FireWire): an Experiment with E-LOTOS
  M. Sighireanu, R. Mateescu

• Towards Mechanical Verification of Parts of the IEEE P1394 Serial Bus
  Lars Kuehne, Jozef Hooman, Willem-Paul de Roever

• Probabilistic Extensions of TE-LOTOS
  Zbigniew Huzar, Jan Magott

• Functionality Bipartition in Basic E-LOTOS
  Monika Kapus-Kolar

• Validation of Hardware Implementations using Formal Description Techniques
  G. Huecas, T. Robles, L.M. Gonzalez, J. Serrano

• Requirement for Service Creation Environments
  Nikolaos Kosmas, Kenneth J. Turner

• An Annotational Extension of SDL 92 to Support a Formal Implementation Specification
  Peter Langendoerfer

• Understanding and Modelling the USB Hub
  Dennis Dams, Rob Gerth, Gertjan Kamsteeg

• Specification and Verification of the CO4 Distributed Knowledge System using LOTOS
  Charles Pecheur (Hubert Garavel)

• Hardware-Software Co-Design for Protocols
  Gyula Csopaki

• Relating Architecture and Specification
  Ken Turner

• Timed μCRL
  Jan-Friso Groote

• Test Case Selection
  Katy Tarnay

• Testing Interoperability
  Mazen Malek

• Testing at LTiV - Research and Application Projects
  Krzysztof Brzezinski

• Firewire Tree Identify Protocol
  Carron Shankland

• Verification of VDM-Style Specifications with PVS
  Savi Maharaj

• Use of Formal Methods in The BOS Project
  Jan Tretmans

Related Pages

• COST 247 Web server, located at the Middle East Technical University (Turkey)

• Web pages of the First COST 247 International Workshop on Applied Formal Methods in System Design, held in Maribor (Slovenia), June 17-19, 1996

• Web pages of the 2nd COST 247 International Workshop on Applied Formal Methods in System Design, held in Zagreb (Croatia), June 18-19, 1997

• COST Home Page

• List of Current and Former Projects of the VASY Team

Back to the VASY Home page