Mapping live sequence chart to coloured petri nets for analysis and verification of embedded systems

ABSTRACT

This paper presents a methodology for mapping the Live Sequence Chart (LSC) language to an equivalent Coloured Petri Net (CPN) model as an approach for analysis and verification of embedded systems' properties. LSC is a language for system specification, allowing one to specify what should happen for all execution of the system as well as the modeling of anti-scenarios. However, analysis and verification of systems' properties are not possible. In order to allow diagnosis of inconsistent specifications, besides simulation, verification and analysis should be considered. Therefore the proposition of a CPN model for LSC allows verification and analysis of systems described in LSC, hence, contributing for increasing designers' confidence on the system development process and reducing risks that may lead to project failure.

REFERENCES

• 1: Extensible Markup Language. http://www.xml.org.
• 2: JDOM API. http://www.jdom.org.
• 3: Luciano Baresi and Mauro Pezzè. Improving uml with petri nets. Electr. Notes Theor. Comput. Sci., 44(4), 2001.
• 4: Y. Bontemps and P. Heymans. Turning high-level live sequence charts into automata. International Conference on Software Engineering, 2002.
• 5: CCITT. Ccitt recommendation z.120: Message sequence chart (msc). Geneva, 1992.
• 6: Werner Damm , David Harel, LSCs: Breathing Life into Message Sequence Charts, Formal Methods in System Design, v.19 n.1, p.45-80, July 2001 [doi>10.1023/A:1011227529550 ]
• 7: Department of Computer Science of University of Aarhus, http://wiki.daimi.au.dk/cpntools/cpntools.wiki. CPN Tools.
• 8: Grady Booch , James Rumbaugh , Ivar Jacobson, The Unified Modeling Language user guide, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1999
• 9: David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9 ]
• 10: David Harel , Eran Gery, Executable Object Modeling with Statecharts, Computer, v.30 n.7, p.31-42, July 1997 [doi>10.1109/2.596624 ]
• 11: David Harel , Rami Marelly, Come, Let's Play: Scenario-Based Programming Using LSC's and the Play-Engine, Springer-Verlag New York, Inc., Secaucus, NJ, 2003
• 12: J. Campos J. Merseguer and E. Mena. Performance evaluation for the design of agent-based systems: A petri net approach. 1998.
• 13: Ivar Jacobson, Object-Oriented Software Engineering: A Use Case Driven Approach, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 2004
• 14: Kurt Jensen, An Introduction to the Practical Use of Coloured Petri Nets, Lectures on Petri Nets II: Applications, Advances in Petri Nets, the volumes are based on the Advanced Course on Petri Nets, p.237-292, September 01, 1996
• 15: Kurt Jensen, An Introduction to the Theoretical Aspects of Coloured Petri Nets, A Decade of Concurrency, Reflections and Perspectives, REX School/Symposium, p.230-272, June 01-04, 1993
• 16: M. N. Oliveira Junior. Desenvolvimento de Um Prottipo para a Medida No Invasiva da Saturao Arterial de Oxignio em Humanos -- Oxmetro de Pulso. MSc Thesis, UFPE, August, 1998.
• 17: T. Murata. Petri nets: Properties, analysis and applications. Lecture Notes in Computer Science; A Decade of Concurrency, 77(4):541--580, April 1989.
• 18: Object Management Group, http://www.omg.org. Documentation of the Unified Modeling Language.
• 19: R. Lins P. Maciel and P. Cunha. Introduo s Redes de Petri e Aplicaes. X Escola de Computao Campinas-SP, 1996.
• 20: Sun Microsystems, http://java.sun.com. Java Technology.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Flow charts; Petri nets
      D.2.4 Software/Program Verification

General Terms:
Design, Languages