Brug af formalismer med prioriteret krav i verifikation og modelbaseret test

PhD: Saulius Pusinskas

 Casestory

1. Purpose of the project
The purpose of the project is to

• Adapt the visual formalism of Live Sequence Charts to capture requirements from communication protocols
• Formalize requirements from existing RFC1 specifications of several protocols, perform emulation in and conversion to timed automata (TA) supported in Uppaal2 environment
• Validate, model check, simulate and use in conformance tests the protocol models that consist of formalized requirements.

2. Background

Requirements for communication protocols are defined by means of textual RFC documents. Up to now, thousands of RFCs have been published, some of them re-defining or obsoleting certain requirements defined by their predecessors. Re- quirement is the smallest part which constitutes the protocol specification.

Formal semantics of LSC is available whose certain details are treated in different ways depending on application field [Damm and Harel, 2001] [Klose and Wittke, 2001] [Bontemps, 2005] [Bunker et al, 2001]. Formalism is used in the areas such as compliance verification of hardware protocol specifications [Bunker et al, 2001], simulation, analysis and synthesis of distributed systems [Harel, 2003] [Bontemps, 2005] and many others.

Powerful tools are available for verification, simulation and conformance testing that operate on system models defined in finite state machines (FSM) or timed automata (TA) formalisms; these tools (Uppaal, SPIN3, HyTech4) have proved successful on a number of industrial cases. To exploit capabilities of these tools on the formalized specifications of communication protocols, translation from LSC formalism to TA is necessary.

3. Perspective
Some of existing tools like REMoRDS [Bontemps, 2005] can generate from the LSC chart a LTL5 formulae ready to submit into the model checker. In our approach the LSC specification shall be translated chart-by-chart into the timed automata (TA) supported by Uppaal, where all the model checking, simulation or testing activities are performed.

Through this project we will

• define the set of constructs from LSC formalism that are suitable to capture the communication protocol requirements
• investigate what types of requirements in RFC and to what extent can be formalized using chosen formalism
• define and perform conversion of requirements from LSC to other formalisms where the specifications can be simulated, verified and used as the oracle in conformance tests
• propose the investigated techniques and formalism to capture requirements from current and future RFC documents

4. Industrial application
Formalism used and tools developed will provide means for those who write or use RFC specifications to manipulate requirements more effciently.

Quality of the implementation derived from the LSC-based specification should prove using the formalism beneficial with respect to manual interpretation of requirements.

The increased development speed and quality of the implemented systems should come as a result of using the formal system model in conformance testing. The existing certified protocol implementations will be optionally re-tested against their formal models to estimate how close the formalised requirements are to the assumedly correct implementation.

Using system specifications in LSC charts should improve quality of the system models and software developed at the Ericsson Denmark A/S (Telebit).

5. Timetable for the project
The 3-year long project consists of annual parts:

1. Analysis of RFC requirements, adaptation of LSC formalism to capture these requirements, development of LSC emulator over Uppaal

Period: 1 September 2004 - 1 September 2005

2. Design of the LSC translator to Uppaal in order to generate models more effcient in verification, simulation and testing. Experimenting with an industrial case: communication protocols (SCTP, DHCP).

Period: 1 September 2005 - 1 September 2006

3. Application of the translation and formalization for several communication protocols

Period: 1 September 2006 - 1 September 2007

Literature

[Bontemps, 2005] Yves Bontemps. ”Relating Inter-Agent and Intra-Agent Specifications (The Case of Live Sequence Charts)”. PhD thesis, University of Namur, Belgium, April 2005.

[Bunker et al, 2001] A. Bunker and G. Gopalakrishnan. Using Live Sequence Charts for Hardware Protocol Specification and Compliance Verification.In IEEE International High Level Design Validation and Test Workshop, pages 95–100, 2001.

[Damm and Harel, 2001] W.Damm and D.Harel. LSCs: Breathing Life into Message Sequence Charts. Formal Methods in System Design, 19, 4580, 2001.

[Harel, 2003] David Harel. Come, let’s Play. Scenario-Based Programming using LSCs and the Play-Engine. ISBN 3-540-00787-3 Springer, 2003.

[Klose and Wittke, 2001] J. Klose, H. Wittke. An Automata Based Interpretation of Live Sequence Charts. Proceedings of TACAS 2001, number 2031 in LNCS. Springer Verlag, 2001.

Notes:

1. Request For Comments
2. www.uppaal.com
3. www.spinroot.com
4. http://embedded.eecs.berkeley.edu/research/hytech/
5. Linear Temporal Logics