|
| volgende >> |
Tijdschrift beschrijving
Alle jaargangen van het bijbehorende tijdschrift
Alle afleveringen van het bijbehorende jaargang
Alle artikelen van de bijbehorende aflevering
Details van artikel 1 van 5 gevonden artikelen
| Titel: |
A Logic Framework for Verification of Timed Algorithms |
| Auteur: |
Anatol Slissenko |
| Verschenen in: |
Fundamenta informaticae |
| Paginering: | Jaargang 62 (2004) nr. 1 pagina's 29-67 |
| Jaar: |
2004-11-30 |
| Inhoud: |
This paper is a survey of research of my colleagues and myself aimed at developing a comprehensive logical framework for the verification of real-time distributed systems. The framework is based on predicate logics with explicit time. To choose such a logic we pursue two goals: first, to make formalization of verification problems rather direct, without unjustified simplifications, and second, to have a logic which permits to describe decidable classes of the verifications problem covering the particular problems we are interested in. Notice that our intention is not to introduce new specification languages, but work directly with those of the user. In this paper we describe First Order Timed Logic (FOTL) that is sufficient to express the main part of verification of systems without uncertainty. The time is continuous (the formalism work as well for discrete time -- in our context this case is less interesting and less efficient from algorithmic viewpoint). We give examples of problems that can be treated, describe how to represent runs of programs in FOTL, introduce decidable classes, discuss aspects of practical efficiency. We conclude with open questions. |
| Uitgever: |
IOS Press |
| Bronbestand: |
Elektronische Wetenschappelijke Tijdschriften |
Details van artikel 1 van 5 gevonden artikelen
| volgende >> |