Formal Methods Forum

Autumn 1998

This is a seminar on formal methods in computer science and engineering organized by the Laboratory for Theoretical Computer Science at HUT. We meet usually on Fridays at 2 p.m. in room B353 in the Computer Science building.

For further information, please contact Ilkka Niemelä.

Program

• 13.11.98 Nisse Husberg: Emma and Maria - Theoretical and Practical Problems in Industrial Analysis

  Abstract: The experiences of applying the Emma SDL analyzer to industrial processes (together with PROD) and the design of the Maria analyzer are discussed. Industrial size systems require formalisms and methods which unfortunately have been almost neglected in academic research and tool design. Tools which can handle these systems are seldom based on formal methods or are very crude. It seems, however, possible to lift the academic methods to more expressive high level formalisms and even automatically translate the industrial description of the system into a formal model which can be verified. The work needed for this should not be underestimated and it must be done as well on the theoretical as the practical level. Expressive efficiency must be combined with computational efficiency in order to get something useful. Especially methods which work directly on high level formalisms and reduce the complexity of the verification seem to be of outmost importance.

• 20.11.98 Teemu Tynjälä: Reachability-based Verification of DSS1 Protocol

  Abstract: Theoretical computer science has developed many formalisms for the challenging task of large system verification. Petri Nets is one such formalism. This work presents modelling and analysis of DSS1 - an ISDN protocol - with Petri Net formalism. The results of the work include methods of modelling communication paths, higher layer service primitives, timers, and transmission errors with Petri nets. Analysis of the protocol model was made more efficient with the use of static precedences. The analysis uncovered three errors in the protocol. These - as well as their corrections - are given during the presentation.

• 04.12.98 Marko Mäkelä: Implementing the Front-End of an SDL Compiler

  Abstract: Errors in large distributed systems are practically impossible to find with simple reasoning or testing, and they can have unexpected consequences that cost lots of money. Traditionally formal methods, which will find even the most obscure errors, have been based on manually derived models of the systems to be analyzed. Many industrial designs have not been formally verified, because the effort of modeling them has been considered too high. Compilers made a revolution in computing by allowing the use of high-level programming languages. Now compiler technology can be applied to make formal methods more accessible for system designers. This work describes the front-end of an SDL compiler, which parses specifications written in SDL and stores them in a syntax tree and performs semantic checks. With the exception of macros, the parser recognizes the whole SDL grammar defined in 1996. Converting the grammar to the LALR(1) form required by the parser generator tool has involved numerous modifications to the grammar and to the lexical analyzer. Special attention has been paid to error tolerance and recovery and to meaningful error reporting. Once finished, the compiler will translate SDL specifications to high-level Petri Net models that can be verified using formal methods.

• 11.12.98, at 3 p.m., Tapio Manner, Nokia Telecommunications: Extending Verification of Industrial Distributed Systems with Formal Methods by Using EMMA

  Abstract: The presentation will report results of the evaluation of the EMMA analyzer in the industrial environment. The purpose of the evaluation was to assess the potential the analyzer offers to the software development process of telecommunication systems at Nokia Telecommunications. The analyzer based on formal methods and the reachability analysis remarkably facilitates the uncovering of problems related to concurrent behavior such as deadlocks, and showing characteristics related to system states. The analyzer offers a promising alternative to increase test coverage in a cost effective manner since with a widely used test driver approach one can practically never reach a 100 percentage coverage. Examples are given which demonstrate error detecting ability of the EMMA analyzer. The analyzer can analyze the parts of software implemented or designed using the TNSDL language with certain restrictions. The restrictions are described and general guidelines of the feasible bypassing plans are presented.