Techniques for Abstracting SDL Specifications

  • Sergiy Boroday
  • Roland Groz
  • Alex Petrenko
  • Yves-Marie Quemener
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2599)


Abstracting the behaviour of a specification is a key technique for dealing with the complexity of such tasks as reachability analysis and test generation. We adapted classical data-flow analysis techniques to abstract variables in SDL processes and addressed the problem of finding conservative state abstractions. Prototype tools have been developed to implement those techniques and applied to simple applications from the field of telecommunications.


Model Check Test Generation Fault Model Finite State Machine Reachability Analysis 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    v. Bochmann G., Das, A. Dssouli R., Dubuc M., Ghedamsi A., Luo G.: Fault Model in Testing. Proceedings of the IFIP IV Workshop on Protocol Test Systems; pp. 17–30, October 1991; Leidschendam, The Netherlands.Google Scholar
  2. 2.
    Bozga M., Fernandez J.-Cl., Ghirvu L., Graf S., Krimm J.-P., Mounier L., Sifakis J.: IF: An Intermediate Representation for SDL and its Applications. Proceedings of SDLFORUM 1999; pp. 423–440, June 1999; Montreal, Canada.Google Scholar
  3. 3.
    Bozga M., Fernandez J.-Cl., Ghirvu L.: State Space Reduction based on Live Variables Analysis. Proceeedings of SAS’99, Venice, Italy. LNCS 1694, pp. 164–178, Springer Verlag.Google Scholar
  4. 4.
    Bozga M.: Vérification symbolique pour les protocoles de communication. PhD Thesis, Grenoble University, 1999.Google Scholar
  5. 5.
    Boroday S., Petrenko A., Groz R., and Quemener Y.-M.: Test Generation for CEFSM Combining Specification and Fault Coverage. Proceedings of IFIP 14th International Conference on Testing of Communicating Systems (TestCom 2002), pp. 355–371, March 2002, Berlin, Germany, Kluwer.Google Scholar
  6. 6.
    Clark E., Grumberg O., and Peled D.: Model Checking. MIT, 1999.Google Scholar
  7. 7.
    Cormen T., Leiserson C., Rivest R.: Introduction to Algorithms. MIT, 1992.Google Scholar
  8. 8.
    Cousot P. and Cousot R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. 4th POPL, pp. 238–252, Los Angeles, USA, 1977, ACM Press.Google Scholar
  9. 9.
    Gill A.: Introduction to the Theory of Finite-State Machines, McGrawHill, New York, 1962.zbMATHGoogle Scholar
  10. 10.
    Grabowski J., Scheurer R., Toggweiler D., and Hogrefe D.: Dealing with the complexity of state space exploration algorithms for SDL systems. Arbeitsberichte des Instituts für mathematische Maschinen-und Datenverarbeitung (Mathematik), Proceedings of the 6th GI/ITG Technical Meeting on Formal Description Techniques for Distributed Systems, June 20-21, 1996, pp. 1–10, Vol. 20, No. 9, University of Erlangen, Germany, May 1996.Google Scholar
  11. 11.
    Kerbrat A., Jéron T., Groz R.: Automated test generation from SDL specifications. Proceedings of the 9th SDL Forum; pp 135–151, June 1999; Montreal, Canada. Elsevier.Google Scholar
  12. 12.
    Loiseaux C., Graf S., Sifakis J., Bouajjani A., and Bensalem S.: Property Preserving Abstractions for the Verification of Concurrent Systems. Formal Methods in System Design, 6, pp. 11–44, 1995.zbMATHCrossRefGoogle Scholar
  13. 13.
    Moundanos D, Abraham J. A., Hoskote Y.: Abtraction Techniques for Validation, Coverage Analysis and Test generation. IEEE Trans. on Computing, Vol. 47, No. 1, Jan. 1998, pp. 2–14.CrossRefGoogle Scholar
  14. 14.
    Oikonomou K. N.: Abstractions of Finite-state Machines and Optimality with Respect to Immediately-Detectable Next-State Faults. IEEE Transactions on Systems, Man, and Cybernetics, Part A, pp. 151–160, Vol. 26, No.1, Jan. 1996.CrossRefGoogle Scholar
  15. 15.
    Petrenko A.: Fault Model-Driven Test Derivation from Finite State Models: Annotated Bibliography. LNCS 2067, Proceedings of the Summer School MOVEP’2000, Modeling and Verification of Parallel Processes; pp. 196–205, June 2000; Nantes, France.Google Scholar
  16. 16.
    Petrenko A., Boroday S., and Groz R.: Confirming configurations in EFSM. Proceedings of the IFIP Joint International Conference on Formal Description Techniques for Distributed Systems (FORTE XII) and Communication Protocols, and Protocol Specification, Testing, and Verification (PSTV XIX); pp. 5–24, October 1999, China. Kluwer.Google Scholar
  17. 17.
    Petrenko A. and Yevtushenko N.: Test Suite Generation for a FSM with a Given Type of Implementation Errors. Proceedings of the IFIP 12th International Symposium on Protocol Specification, Testing, and Verification; pp. 229–243, 1992; USA. North-Holland.Google Scholar
  18. 18.
    Rusu V., du Bousquet L., and Jeron T.: An Approach to Symbolic Test Generation. International Conference on Integrating Formal Methods (IFM’00), Springer Verlag, LNCS 1945, pp. 338–357, Novembre 2000.Google Scholar
  19. 19.
    Tip F.: A survey of program slicing techniques. Journal of Programming Languages, 3(3), pp. 121–189, September 1995.Google Scholar
  20. 20.
    Wang X.: Abstraction of Variables in SDL. Master Thesis, McGill University, 2001.Google Scholar
  21. 21.
    Yun H.: State abstraction in SDL. Master Thesis, Université de Montréal, 2001.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Sergiy Boroday
    • 1
  • Roland Groz
    • 2
  • Alex Petrenko
    • 1
  • Yves-Marie Quemener
    • 3
  1. 1.CRIM, 550 Sherbrooke WestMontrealCanada
  2. 2.INPG-ENSIMAG, LabSt Martin d’Hères CedexFrance
  3. 3.France TélécomLannion cedexFrance

Personalised recommendations