Muffy Calder
ABSTRACT
We show how SPIN is applied to analyse the behaviour of a real software artifact — feature interaction in telecommunications services. We demonstrate how minimal abstraction techniques can greatly reduce the cost of model-checking, and how analysis can be performed automatically using scripts.
- 1.L. G. Bouma and H. Velthuijsen, editors. Feature Interactions in Telecommunications Systems. IOS Press (Amsterdam), May 1994.]] Google Scholar
Digital Library
- 2.M. Calder and E. Magill, editors. Feature Interactions in Telecommunications and Software Systems, volume VI. IOS Press, Amsterdam, 2000.]] Google ScholarDigital Library
- 3.M. Calder, E. Magill, and D. Marples. A hybrid approach to software interworking problems: Managing interactions between legacy and evolving telecommunications software. IEE Proceedings - Software, 146(3):167-180, June 1999.]]Google ScholarCross Ref
- 4.Muffy Calder and Alice Miller. Analysing a basic call protocol using Promela/ XSpin. In {15}, pages 169--181, 1998.]]Google Scholar
- 5.E. J. Cameron, N. Griffeth, Y.-J. Lin, M. E. Nilson, and W. K. Schnure. A feature interaction benchmark for IN and beyond. In {1}, pages 1-23, May 1994.]]Google Scholar
- 6.E.M. Clarke, O. Gumberg, and D Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512-1542, September 1994.]] Google ScholarDigital Library
- 7.Costas Courcoubetis, editor. Proceedings of the Fifth International Conference on Computer Aided Verification (CAV `93), volume 697 of Lecture Notes in Computer Science, Elounda,Greece, June/July 1993. Springer-Verlag.]] Google ScholarDigital Library
- 8.P. Dini, R. Boutaba, and L. Logrippo, editors. Feature Interactions in Telecommunication Networks IV. IOS Press (Amsterdam), June 1997.]] Google ScholarDigital Library
- 9.K. Etessami. Stutter-invariant languages, w-automata, and temporal logic. In {12}, pages 236-248, 1999.]] Google ScholarDigital Library
- 10.A. Felty and K. Namjoshi. Feature specification and automatic con ict detection.]]Google Scholar
- 11.Susanne Graf and Claire Loiseaux. A tool for symbolic program verificaion and abstration. In {7}, pages = 71-84, year = 1993,.]] Google ScholarDigital Library
- 12.Nicolas Halbwachs and Doron Peled, editors. Proceedings of the eleventh International Conference on Computer-aided Verification (CAV `99), volume 1633 of Lecture Notes in Computer Science, Trento, Italy, July 1999. Springer-Verlag.]] Google ScholarDigital Library
- 13.Constance L. Heitmeyer, James Jr. Kirby, Bruce Labaw, Myla Archer, and Ramesh Bharadwaj. Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Transactions on Software Engineering, 24(11), November 1998.]] Google ScholarDigital Library
- 14.D. Hogrefe and S. Leue, editors. Proceedings of the Seventh International Conference on Formal Description Techniques (FORTE '94), volume 6 of International Federation For Information Processing, Berne, Switzerland, October 1994. Kluwer Academic Publishers.]] Google ScholarDigital Library
- 15.Gerard Holzmann, Elie Najm, and Ahmed Serhrouchni, editors. Proceedings of the 4th Workshop on Automata Theoretic Verification with the Spin Model Checker (SPIN `98), Paris, France, November 1998.]]Google Scholar
- 16.Gerard J. Holzmann. The model checker Spin. IEEE Transactions on Software Engineering, 23(5):279-295, May 1997.]] Google ScholarDigital Library
- 17.Gerard J. Holzmann and Doron Peled. An improvement in formal verification. In {14}, pages 197-211, 1994.]] Google ScholarDigital Library
- 18.G.J. Holzmann and Margaret H. Smith. A practical method for the verification of event-driven software. In Proceedings of the 1999 international conference on Software engineering (ICSE99), pages 597-607, Los Angeles, CA, USA, May 1999. ACM Press.]] Google ScholarDigital Library
- 19.IN Distributed Functional Plane Architecture, recommmendation q.1204, ITU-T edition, March 1992.]]Google Scholar
- 20.K. Kimbler and L.G. Bouma, editors. Feature Interactions in Telecommunications and Software Systems V. IOS Press (Amsterdam), September 1998.]] Google ScholarDigital Library
- 21.M. Kolberg, E. H. Magill, D. Marples, and S. Reiff. Results of the second feature interaction contest. In {2}, pages 311-325, May 2000.]]Google Scholar
- 22.M. Plath and M. Ryan. Plug-and-play features. In {20}, pages 150-164, 1998.]]Google Scholar
- 23.M. Thomas. Modelling and analysing user views of telecommunications services.]]Google Scholar
- Using SPIN for feature interaction analysis—a case study
Recommendations
Assertion Based Verification using Yosys: A Case Study from Nuclear Domain
ISEC '23: Proceedings of the 16th Innovations in Software Engineering ConferenceAssertion Based Verification is a design methodology that integrates Formal Methods as part of the design process. As each module is designed, the designer expresses the functional, structural and interface requirements of the module as logical formulas ...
Feature interaction detection by pairwise analysis of LTL properties: a case study
A Promela specification and a set of temporal properties are developed for a basic call service with a number of features. The properties are expressed in the logic LTL.Interactions between features are detected by pairwise analysis of features and ...
Model Checking in Practice: Analysis of Generic Bootloader Using SPIN
Formal Methods and Software EngineeringAbstractThis work presents a case study of the use of model checking for analyzing an industrial software, the Generic Bootloader. Analysis of the software have been carried out using the automated verification system SPIN. A model of the software has ...
Comments