Paper Info
Title
OCL-based runtime monitoring of applications with protocol state machines
Abstract
This paper presents an approach that enables users to monitor and verify the behavior of an application running on a virtual machine (like the Java virtual machine) at an abstract model level. Models for object-oriented implementations are often used as a foundation for formal verification approaches. Our work allows the developer to verify whether a model corresponds to a concrete implementation by validating assumptions about model structure and behavior. In previous work, we focused on (a) the validation of static model properties by monitoring invariants and (b) basic dynamic properties by specifying pre- and postconditions of an operation. In this paper, we extend our work in order to verify and validate advanced dynamic properties, i.,e., properties of sequences of operation calls. This is achieved by integrating support for monitoring UML protocol state machines into our basic validation engine.
Year
DOI
Venue
2012
10.1007/978-3-642-31491-9_29
ECMFA
Keywords
Field
DocType
basic validation engine,model structure,dynamic property,abstract model level,static model property,basic dynamic property,java virtual machine,previous work,uml protocol state machine,ocl-based runtime monitoring,model corresponds,state machine
Programming language,Virtual machine,Unified Modeling Language,Computer science,Finite-state machine,Implementation,Runtime verification,Symbolic execution,Java Modeling Language,Distributed computing,Formal verification
Conference
Citations 
PageRank 
References 
10
0.66
22
Authors
3
Name
Order
Citations
PageRank
Lars Hamann123420.17
Oliver Hofrichter2265.12
Martin Gogolla32398578.76