Slicing Timed Systems

Issue title: Concurrency Specification and Programming (CS&P 2003)

Article type: Research Article

Authors: Janowska, Agata | Janowski, Paweł

Affiliations: Institute of Informatics, Warsaw University, Banacha 2, 02-097 Warsaw, Poland

Abstract: This paper presents a method of slicing timed systems to create reduced models for model checking verification. The reduction is made at the very beginning of the verification process and this makes it beneficial and effective in handling the state explosion problem. The method uses techniques of static analysis to examine the syntax of a program and to remove irrelevant fragments of the code. The timed extension of the classical slicing definition is given and applied to Intermediate Language of the verification system Verics and Estelle specification language.

Keywords: static analysis, program slicing, system verification, timed systems, timed automata

Journal: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 187-210, 2004