Wyniki wyszukiwania - BazTech

Ograniczanie wyników

1 Fundamenta Informaticae

1 2017

Znaleziono wyników: 1

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: parameterized property

Sortuj według:

Ogranicz wyniki do:

Monitoring with Parametrized Extended Life Sequence Charts

Chai M., Schlingloff B. -H.

Fundamenta Informaticae

2017

Vol. 153, nr 3

173--198

Runtime verification is a lightweight formal method that checks whether an execution of a system satisfies a given property. A challenge in building a runtime verification system is to define a suitable monitoring specification language, i.e., a language that is expressive, of reasonable complexity, and easy to understand. In this paper, we extend live sequence charts (LSCs, [1]) for the specification of properties in systems monitoring. We define Parametrized extended LSCs (PeLSCs) by introducing the notions of necessary prechart, concatenation, and conditionand assignment-structure. With these PeLSCs, necessary and sufficient conditions of certain observations, and parametric properties can be specified in an intuitive way. We prove some results about the expressiveness of extended LSCs. In particular, we show that LSCs with necessary precharts are strictly more expressive than standard LSCs, and that iteration-free extended LSCs have the same expressive power as linear temporal logic (LTL). To generate monitors, we develop translations of PeLSCs into hybrid logic. We show that the complexity of the word problem of PeLSCs is linear with respect to the length of input traces, thus our formalism is well-suited for online monitoring of communicating systems.