Impartial Anticipation in Runtime-Verification.
In this paper, a uniform approach for synthesizing monitors checking correctness properties specified in linear-time logics at runtime is provided. Therefore, a generic three-valued semantics is introduced reflecting the idea that prefixes of infinite computations are checked. Then a conceptual fram...
| मुख्य लेखकों: | , , |
|---|---|
| अन्य लेखक: | |
| स्वरूप: | Journal article |
| भाषा: | English |
| प्रकाशित: |
Springer
2008
|
| _version_ | 1826280430861549568 |
|---|---|
| author | Dong, W Leucker, M Schallhart, C |
| author2 | Cha, S |
| author_facet | Cha, S Dong, W Leucker, M Schallhart, C |
| author_sort | Dong, W |
| collection | OXFORD |
| description | In this paper, a uniform approach for synthesizing monitors checking correctness properties specified in linear-time logics at runtime is provided. Therefore, a generic three-valued semantics is introduced reflecting the idea that prefixes of infinite computations are checked. Then a conceptual framework to synthesize monitors from a logical specification to check an execution incrementally is established, with special focus on resorting to the automata-theoretic approach. The merits of the presented framework are shown by providing monitor synthesis approaches for a variety of different logics such as LTL, the linear-time μ-calculus, PLTLmod, SiS, and RLTL. © 2008 Springer Berlin Heidelberg. |
| first_indexed | 2024-03-07T00:13:36Z |
| format | Journal article |
| id | oxford-uuid:7a15a57a-013c-4fba-aa02-19339cec2d71 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T00:13:36Z |
| publishDate | 2008 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:7a15a57a-013c-4fba-aa02-19339cec2d712022-03-26T20:41:37ZImpartial Anticipation in Runtime-Verification.Journal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:7a15a57a-013c-4fba-aa02-19339cec2d71EnglishSymplectic Elements at OxfordSpringer2008Dong, WLeucker, MSchallhart, CCha, SChoi, JKim, MLee, IViswanathan, MIn this paper, a uniform approach for synthesizing monitors checking correctness properties specified in linear-time logics at runtime is provided. Therefore, a generic three-valued semantics is introduced reflecting the idea that prefixes of infinite computations are checked. Then a conceptual framework to synthesize monitors from a logical specification to check an execution incrementally is established, with special focus on resorting to the automata-theoretic approach. The merits of the presented framework are shown by providing monitor synthesis approaches for a variety of different logics such as LTL, the linear-time μ-calculus, PLTLmod, SiS, and RLTL. © 2008 Springer Berlin Heidelberg. |
| spellingShingle | Dong, W Leucker, M Schallhart, C Impartial Anticipation in Runtime-Verification. |
| title | Impartial Anticipation in Runtime-Verification. |
| title_full | Impartial Anticipation in Runtime-Verification. |
| title_fullStr | Impartial Anticipation in Runtime-Verification. |
| title_full_unstemmed | Impartial Anticipation in Runtime-Verification. |
| title_short | Impartial Anticipation in Runtime-Verification. |
| title_sort | impartial anticipation in runtime verification |
| work_keys_str_mv | AT dongw impartialanticipationinruntimeverification AT leuckerm impartialanticipationinruntimeverification AT schallhartc impartialanticipationinruntimeverification |