|
The academic and industrial R&D communities are currently paying close attention to the use of automatic verification tools such as model checkers to cope with challenges arising during the development of distributed and embedded systems. Since full coverage of software behavior is unfeasible in many large applications, new approaches are being proposed which trade coverage for scalability. Automatic trace conformance-analysis and run-time monitoring belong to this class of proposals where execution traces are compared against formally specified requirements. For instance, MaC tool [MAC], TempRover [Rover] and PathExplorer[PAX] check if event traces satisfy specifications based on some sort of past temporal logic, monMSC [MON] checks conformance of event-logs to Message Sequence Chart Graphs specs., while AsmL Test [ASML] performs state-based trace analysis for Abstract State Machine specifications. In all cases, in order to take advantage of these state-of-the-art tools, developers need their applications to generate appropriate event or state logs. Our goal in this project is to build a novel tool that enables distributed embedded applications running on the CE .NET operating system and the .NET Compact Framework to transparently register relevant timestamped events. In order to show how this instrumentation technology can participate in a larger tool-set, we demonstrate, as part of our implementation, how produced event logs can be fed to different kinds of visualization and conformance-checking tools. For instance:
Traces can be presented in a user-friendly fashion using Message Sequence Charts editors provided by CASE tools such as Telelogic Tau, Rational Rose RT, etc.
Generated traces can be checked for protocol conformance against hMSCs (ITU Z.120 [MSC]) specifications using a tool recently developed by our research group ([MON]). A typical use of these features would be the detection and diagnosis of event ordering and timing discrepancies with respect to defined application-level protocols given in terms of hMSCs and to measure coverage during integration testing of distributed systems.
Generated traces can be automatically analyzed to check whether they entail scenarios which violate RT-requirements such as freshness, bounded response, correlation, etc. Those properties can be given in terms of a visual language proposed by our research group to define complex event-based requirements for RT-systems. A monitoring tool based on the pattern language is work in progress.
|