Scipediacontent: Scipediacontent moved page Draft Content 287259681 to Ouaknine 2007a

2020-10-14T13:02:04Z

Scipediacontent moved page Draft Content 287259681 to Ouaknine 2007a

Scipediacontent: Created page with " == Abstract == We study the digitisation of dense-time behaviours of timed processes, and show how this leads to exact verification methods for a large class of dense-time s..."

2020-10-14T13:02:02Z

Created page with " == Abstract == We study the digitisation of dense-time behaviours of timed processes, and show how this leads to exact verification methods for a large class of dense-time s..."

New page

== Abstract ==

We study the digitisation of dense-time behaviours of timed processes, and show how this leads to exact verification methods for a large class of dense-time specifications. These specifications are all closed under inverse digitisation, a robustness property first introduced by Henzinger, Manna, and Pnueli (on timed traces), and extended here to timed failures, enabling us to consider liveness issues in addition to safety properties. We discuss a corresponding model checking algorithm and show that, in many cases, automated verification of such dense-time specifications can in fact be directly performed on the model checker FDR (a commercial product of Formal Systems (Europe) Ltd.). We illustrate this with a small case study (the railway level crossing problem). Finally, we show that integral--or digitised--behaviours are fully abstract with respect to specifications closed under inverse digitisation, and relate this to the efficiency of our model checking algorithm.

Document type: Part of book or chapter of book

== Full document ==
<pdf>Media:Draft_Content_287259681-beopen693-6401-document.pdf</pdf>

== Original document ==

The different versions of the original document can be found in:

* [https://link.springer.com/content/pdf/10.1007%2F3-540-46002-0_4.pdf https://link.springer.com/content/pdf/10.1007%2F3-540-46002-0_4.pdf]

← Older revision	Revision as of 13:02, 14 October 2020
(No difference)

Ouaknine 2007a - Revision history

Scipediacontent: Scipediacontent moved page Draft Content 287259681 to Ouaknine 2007a

Scipediacontent: Created page with " == Abstract == We study the digitisation of dense-time behaviours of timed processes, and show how this leads to exact verification methods for a large class of dense-time s..."