next up previous
Next: About this document ... Up: Formal Methods for Communication Previous: Conclusions


M. Ardis, J. Chaves, L. Jagadeesan, P. Mataga, C. Puchol, M. Staskauskas, and J. von Olnhausen.
A framework for evaluating specification methods for reactive systems - experience report.
IEEE Transactions on Software Engineering, 22(6):378-389, June 1996.

S. Aujla, T. Bryant, and L. Semmens.
Applying formal methods within structured development.
Journal on Selected Areas in Communications, 12(2):258-264, February 1994.

P. Bates.
Debugging heterogeneous distributed systems using event-based models of behavior.
ACM Transactions on Computer Systems, 13(1):1-31, February 1995.

LATA switching systems generic requirements (LSSGR).
Bellcore, TR-TSY-000064, 1992.

R. Bennett, J. Lindner, R. Michelsen, and D. Rypka.
SDL in 5ESS switching system development.
In Proceedings of the 6th International Conference on Software Engineering for Telecommunication Switching Systems, Eindhoven, Netherlands, April 1986.

J. Blom, R. Bol, and L. Kempe.
Automatic detection of feature interactions in temporal logic.
In K. Cheng and T. Ohta, editors, Feature interactions in Telecommunications Systems III, pages 1-19. IOS Press, 1995.

J. Blom, B. Jonsson, and L. Kempe.
Using temporal logic for modular specification of telephone services.
In L. Bouma and H. Velthuijsen, editors, Feature Interactions in Telecommunications systems, pages 197-213. IOS Press, 1994.

P. Bosco, G. Martini, D. LoGiudice, and C. Moiso.
ACE: An environment for specifying, developing and generating TINA services.
In Proceedings of the Fifth International Symposium on Integrated Network Management, San Diego, CA, USA, May 1997.

L. Bouma and Velthuijsen, editors.
Feature Interactions in Telecommunications Systems. IOS Press, 1994.

L. Bouma and J. Zuidweg.
Formal analysis of feature interactions by model checking.
In Proceedings of the First International Workshop on Feature Interactions in Telecommunications Systems, St. Petersburg, FL, USA, December 1992.

W. Bouma, W. Levelt, A. Melisse, K. Middelburg, and L. Verhaard.
Formalization of properties for feature interaction detection: Experience in a real-life situation.
In H.-J. Kugler, A. Mullery, and N. Niebert, editors, Towards a Pan-European Telecommunication Service Infrastructure - IS&N'94, number 851 in Lecture Notes in Computer Science, pages 393-405. Springer-Verlag, 1994.

K. Braithwaite and J. Atlee.
Towards automated detection of feature interactions.
In [9], pages 36-59. IOS Press, 1994.

C. Capellmann, P. Combes, J. Pettersson, B. Renard, and J. Ruiz.
Consistent interaction detection - a comprehensive approach integrated with service creation.
In [22], pages 183-197. IOS Press, 1997.

CCITT Recommendation Z.100.
Specification and Description Language SDL.
CCITT SG X, Contribution Com X-R15-E, 1987.

K. Cheng.
Towards a formal model for incremental service specification and interaction management support.
In [9], pages 152-166. IOS Press, 1994.

K. Cheng and T. Ohta, editors.
Feature Interactions in Telecommunications Systems III. IOS Press, 1995.

E. Clarke and J. Wing.
Formal methods: State of the art and future directions.
ACM Computing Surveys, 28(4):626-643, December 1996.

D. Coleman, P. Arnold, S. Bodoff, C. Dollin, H. Gilchrist, F. Hayes, and P. Jeremaes.
Object-oriented Development: The FUSION method.
Prentice-Hall, 1994.

F. Dietrich, X. Logean, and J.-P. Hubaux.
Modelling and testing object-oriented distributed systems with linear-time temporal logic.
Submitted to "Theory and Practice of Object Systems.

F. Dietrich, X. Logean, and J.-P. Hubaux.
Testing temporal logic properties in distributed systems.
In IFIP International Workshop on Testing of Communicating Systems (IWTCS), Tomsk, Russia, August 1998.

L. Dillon and Q. Yu.
Oracles for checking temporal properties of concurrent systems.
In Proceedings of the 2nd ACM SIGSOFT Symposium on Foundations of Software Engineering, volume 19, pages 140-153, December 1994.

P. Dini, R. Boutaba, and L. Logrippo, editors.
Feature Interactions in Telecommunication Networks IV. IOS Press, 1997.

A. Eberlein, M. Crowther, and F. Halsall.
Development of new telecommunications services using an expert system.
BT Technology Journal, 15(1):217-222, January 1997.

P.-A. Etique.
Service Specification, Verification and Validation for the Intelligent Network.
PhD thesis, Swiss Federal Institute of Technology, Lausanne, 1995.

M. Faci and L. Logrippo.
Specifying features and analysing their interactions in a LOTOS environment.
In [9], pages 136-151. IOS Press, 1994.

M. Faci, L. Logrippo, and B. Stépien.
Formal specification of telephone systems in LOTOS: The constraint-oriented approach.
Computer Networks and ISDN Systems, pages 53-67, 1991.

M. Faci, L. Logrippo, and B. Stépien.
Structural models for specifying telephone systems.
Computer Networks and ISDN Systems, pages 501-528, 1997.

Proceedings International Workshop on Feature Interactions in Telecommunications Software Systems, St. Petersburg, FL, December 1992.

A. Flora-Holmquist, J. O'Grady, and M. Staskauskas.
Telecommunications software design using virtual finite state machines.
In Proceedings of the International Switching Symposium (ISS95), Berlin, Germany, pages 103-107, April 1995.

Fault-Tolerant CORBA, Draft Document, OMG, 1999.

R. Glass.
Formal methods are a surrogate for a more serious software concern.
IEEE Computer, pages 19-20, April 1996.

J. Goguen and Luqi.
Formal methods and social context in software development.
In TAP-SOFT'95: 6th International Conference on Theory and Practice of Software Development, number 915 in Lecture Notes in Computer Science, pages 62-81. Springer-Verlag, May 1995.

J.-Ch. Grégoire and M. Ferguson.
Neglected topics of feature interactions: Mechanisms, architectures, requirements.
In P. Dini, R. Boutaba, and L. Logrippo, editors, Feature Interactions in Telecommunication Networks IV, pages 3-12. IOS Press, 1997.

D. Gries.
The need for eduation in useful formal logic.
IEEE Computer, April 1996.

N. Griffeth and Y.-J. Lin.
Extending telecommunications systems: The feature-interaction problem.
IEEE Computer, 26(8):14-18, August 1993.

G. Holzmann.
Design and Validation of Computer Protocols.
Prentice-Hall, 1991.

G. Holzmann.
The theory and practice of a formal method: NewCoRe.
In Proceedings of the IFIP World Computer Congress, volume I, pages 35-44, Hamburg, Germany, August 1994. North-Holland Publ., Amsterdam, The Netherlands.

G. Holzmann and J. Patti.
Validating SDL specifications: An experiment.
In Proceedings of the Ninth International Workshop on Protocol Specification, Testing and Verification, 1989.

J.-P. Hubaux, C. Gbaguidi, S. Koppenhöfer, and J.-Y. Le Boudec.
The impact of the internet on telecommunications architectures.
Computer Networks and ISDN Systems, 1998.
To appear.

ISO IS 8807.
LOTOS - A formal description technique based on the temporal ordering of observational behavior.
ISO/TC97/SC21, November 1988.

ISO IS 9074.
Estelle - A formal description technique based on an extended state transition model.
ISO/TC97/SC21, 1989.

General recommendations on telephone switching and signalling, Intelligent Network - Q-Series Intelligent Network Q.1200 - Q.1290, 1993.

L. Jagadeesan, C. Puchol, and J. Olnhausen.
A formal approach to reactive systems software: A telecommunications application in ESTEREL.
Journal of Formal Methods in System Design, 1995.

Jean-Marc Jézéquel, Alain Le Guennec, and François Pennaneac'h.
Validating distributed software modeled with UML.
In Pierre-Alain Muller and Jean Bézivin, editors, Proceedings of UML'98 International Workshop, Mulhouse, France, June 3 - 4, 1998, pages 331-340. ESSAIM, Mulhouse, France, 1998.

Y. Kawarasaki and T. Ohta.
A new proposal for feature interaction detection and elimination.
In [16], pages 127-139. IOS Press, 1995.

J. Keller and O. Dubuisson.
Formal description of OSI management information structure as a prerequisite for formal specifications of TMN interfaces.
In Towards a Pan-European Telecommunication Service Infrastructure - IS&N'94, number 851 in Lecture Notes in Computer Science, pages 433-442. Springer-Verlag, 1994.

B. Kelly, M. Crowther, J. King, R. Masson, and J. DeLapeyre.
Service validation and testing.
In [16]. IOS Press, 1994.

B. Kitson, P. Leydekkers, N. Mercouroff, and F. Ruano.
TINA Object Definition Language (TINA-ODL) Manual 1.3.
TINA-C, June 1995.

F. Koch.
Spezifizierung offener verteilter Systeme aus Sicht des ODP Computational Viewpoint.
GMD-Studien Nr. 243, Gesellschaft für Mathematik und Datenverarbeitung, October 1994.

E. Koerner and L. Strick.
Applying LOTOS to the design of TINA applications.
In H. Bowman and J. Derrick, editors, Proceedings of Second IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS97), pages 455-466. Chapman & Hall, 1997.

D. Kuhn.
Sources of failure in the public switched telephone network.
Computer, 30(4):31-36, April 1997.

L. Lamport.
TLA in pictures.
IEEE Transactions on Software Engineering, pages 768-775, September 1995.

F. Lin and Y.-J. Lin.
A building block approach to detecting and resolving feature interactions.
In [9]. IOS Press, 1994.

X. Logean, F. Dietrich, and J.-P. Hubaux.
TINA service validation: The ErnesTINA project.
In IEEE ICC Conference, Atlanta, June 1998.

X. Logean, F. Dietrich, J.-P. Hubaux, S. Grisouard, and P.-A. Etique.
On applying formal techniques to the development of hybrid services: Challenges and directions.
IEEE Communications Magazine, 37(7), July 1999.

X. Logean, F. Dietrich, and S. Koppenhoefer.
Run-time monitoring of distributed applications.
In Proceedings of Middleware`98, Lake District, England, September 1998.

J. Maisonneuve, S. Chabridon, and P. Leveillé.
The PERCO platform.
In ISORC'99, St. Malo, The 2nd IEEE International Symposium on Object-oriented Real-time distributed Computing, May 1999.

Z. Manna and A. Pnueli.
On the faithfulness of formal models.
In Mathematical Foundations of Computer Science, number 520 in Lecture Notes in Computer Science, pages 28-42. Springer-Verlag, 1991.

C. Middelburg.
A simple language for expressing properties of telecommunication services and features.
Technical Report 94-PU-356, PTT Research, April 1994.

H. Mulder.
TINA-C Glossary of Terms, Version 2.0.
TINA-C, January 1997.

M. Nakamura, Y. Kakuda, and T. Kikuno.
Petri-net based detection method for non-deterministic feature interactions and its experimental evaluation.
In P. Dini, R. Boutaba, and L. Logrippo, editors, Feature Interactions in Telecommunication Networks IV, pages 138-152. IOS Press, 1997.

T. Ohta and Y. Harada.
Classification, detection and resolution of service interactions in telecommunication services.
In [9]. IOS Press, 1994.

G. Parkin and S. Austin.
Overview: Survey of formal methods in industry.
Technical report, National Physical Laboratory, Teddington, Middlesex, U.K., May 1993.

IONA Technologies PLC.
OrbixWeb Programmer's Guide, September 1998.

Real-Time CORBA, Joint Revised Submission.
Available at, December 1998.

R. Saracco, J. Smith, and R. Reed.
Telecommunications System Engineering using SDL.
North-Holland, 1989.

R. Sinnott and M. Kolberg.
Engineering telecommunication services with SDL.
In Proceedings of the Conference on Formal Methods for Open,Object-based Distributed Systems (FMOODS'99), 1999.

IEEE Computer Society.
Computer magazine, April 1996.

IEEE Computer Society.
Communications magazine, July 1999.

B. Steffen, T. Margaria, A. Claßen, V. Braun, and M. Reitenspieß.
A constraint-oriented service creation environment.
In PACT'96, 2nd International Conference on Practical Application of Constraint Technology, London, UK, 1996.

B. Stepien, K. Farooqui, and L. Logrippo.
An experience modelling telecommunications systems using ODP-DLcomp.
In E. Najm and J.-B. Stefani, editors, Formal Methods for Open Object-based Distributed Systems, pages 221-228. Chapman & Hall, 1997.



P. Zave.
Secrets of call forwarding: A specification case study.
In G. Bochmann, R. Dssouli, and O. Rafiq, editors, Formal Description Techniques VIII, pages 169-184. Chapman & Hall, 1996.

Falk Dietrich