Temporal skeletons for verifying time

This paper presents an intermediate notation used in a framework for verification of real-time properties. The framework aims at overcoming the need for the framework user to have significant knowledge of the verification specific detail that formal verification at some level is bound to impose on a model. In order to accomplish this, model extraction from source code of an initial formal model, a timing skeleton, is made automatically. The model refinement needed to transform the temporal skeleton into a model that can be verified is not done imy. This allows postponement of the abstraction and specialisation needed for the verification which further improves the readability of the skeleton. The purpose of the timing skeleton is that it easily can be validated to represent the source code it was created from. The timing skeleton is then automatically refined with verification detail, and then hidden for the user, transformed into the notation of a verification tool. This t...

• Type: Conference
• Year: 2005
• Where: SIGADA
• Authors: Gustaf Naeser, Kristina Lundqvist, Lars Asplund
• Keywords: Initial Formal Model, SIGADA 2005, Source Code, Timing Skeleton