Volume

Dagstuhl Seminar Proceedings, Volume 7011

Publication Details

  • published at: 2008-02-06
  • Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik

Access Numbers

Documents

No documents found matching your filter selection.
Document
DOI: 10.4230/DagSemProc.07011.1
07011 Abstracts Collection – Runtime Verification

Authors: Bernd Finkbeiner, Klaus Havelund, Grigore Rosu, and Oleg Sokolsky

Abstract
From January 2--6 2007 the Dagstuhl Seminar 07011 {\em `Runtime Verification'} was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar have been put together in this paper. The first section is an executive summary that describes the seminar topics in general.
Cite as

Bernd Finkbeiner, Klaus Havelund, Grigore Rosu, and Oleg Sokolsky. 07011 Abstracts Collection – Runtime Verification. In Runtime Verification. Dagstuhl Seminar Proceedings, Volume 7011, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{finkbeiner_et_al:DagSemProc.07011.1,
  author =	{Finkbeiner, Bernd and Havelund, Klaus and Rosu, Grigore and Sokolsky, Oleg},
  title =	{{07011 Abstracts Collection – Runtime Verification}},
  booktitle =	{Runtime Verification},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7011},
  editor =	{Bernd Finkbeiner and Klaus Havelund and Grigore Rosu and Oleg Sokolsky},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07011.1},
  URN =		{urn:nbn:de:0030-drops-13764},
  doi =		{10.4230/DagSemProc.07011.1},
  annote =	{Keywords: Program monitoring, dynamic program analysis, specification languages and logics, concurrency errors, program instrumentation, aspect-oriented programming, test oracles, fault protection, dynamic specification learning, combining static and dynamic analysis}
}
Document
DOI: 10.4230/DagSemProc.07011.2
07011 Executive Summary – Runtime Verification

Authors: Bernd Finkbeiner, Klaus Havelund, Grigore Rosu, and Oleg Sokolsky

Abstract
From January 2 to January 6, 2007, the Dagstuhl Seminar 07011 "Runtime Verification" was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. Over the past few years, runtime verification has emerged as a focused subject in program analysis that bridges the gap between the complexity-haunted field of fully formal verification methods and the ad-hoc field of testing. Other terms for this subject are: program monitoring, dynamic program analysis, and runtime analysis. Thirty researchers participated in the seminar and discussed their recent work and recent trends in runtime verification.
Cite as

Bernd Finkbeiner, Klaus Havelund, Grigore Rosu, and Oleg Sokolsky. 07011 Executive Summary – Runtime Verification. In Runtime Verification. Dagstuhl Seminar Proceedings, Volume 7011, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{finkbeiner_et_al:DagSemProc.07011.2,
  author =	{Finkbeiner, Bernd and Havelund, Klaus and Rosu, Grigore and Sokolsky, Oleg},
  title =	{{07011 Executive Summary – Runtime Verification}},
  booktitle =	{Runtime Verification},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7011},
  editor =	{Bernd Finkbeiner and Klaus Havelund and Grigore Rosu and Oleg Sokolsky},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07011.2},
  URN =		{urn:nbn:de:0030-drops-13699},
  doi =		{10.4230/DagSemProc.07011.2},
  annote =	{Keywords: Program monitoring, dynamic program analysis, specification languages and logics, concurrency errors, program instrumentation, aspect-oriented program}
}
Document
DOI: 10.4230/DagSemProc.07011.3
Monitoring, Fault Diagnosis and Testing Real-time Systems using Analog and Digital Clocks

Authors: Stavros Tripakis

Abstract
We give an overview of known methods for monitoring, fault diagnosis and testing problems for real-time systems using timed automata as the main model. We present techniques for constructing monitors/diagnosers/testers with analog or digital clocks. We list a number of open problems in the field.
Cite as

Stavros Tripakis. Monitoring, Fault Diagnosis and Testing Real-time Systems using Analog and Digital Clocks. In Runtime Verification. Dagstuhl Seminar Proceedings, Volume 7011, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{tripakis:DagSemProc.07011.3,
  author =	{Tripakis, Stavros},
  title =	{{Monitoring, Fault Diagnosis and Testing Real-time Systems using Analog and Digital Clocks}},
  booktitle =	{Runtime Verification},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7011},
  editor =	{Bernd Finkbeiner and Klaus Havelund and Grigore Rosu and Oleg Sokolsky},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07011.3},
  URN =		{urn:nbn:de:0030-drops-13705},
  doi =		{10.4230/DagSemProc.07011.3},
  annote =	{Keywords: Monitoring, fault diagnosis, testing, timed automata}
}
Document
DOI: 10.4230/DagSemProc.07011.4
Runtime Verification for Wireless Sensor Network Applications

Authors: Oleg Sokolsky, Usa Sammapun, John Regehr, and Insup Lee

Abstract
We present a case study that considers the application of runtime verification technology to a wireless sensor application. The case study is performed using the SURGE TinyOS application for multi-hop routing, which executes on the Avrora TinyOS simulator. We discuss the problems we have encountered in the course of case study. The problems include unclear correctness properties for wireless network applications (indicating ad hoc development process) and inadequate tool support. A wireless sensor network usually comprises of a collection of tiny devices with built-in processors that can gather physical and environment information such as temperature, light, sound, etc., and communicate with one another over radio. Many wireless sensor network applications sit on top of an operating system called TinyOS and are mostly written in nesC, an extension of C that provides a component-based programming paradigm. Most of wireless sensor network applications are developed and tested on a simulator before they are deployed in the environment because testing and debugging directly on physical devices are very difficult, especially when the network consists of many nodes, and may not provide enough information for debugging. A simulator usually produces detailed execution information and can help find errors. However, even with the simulator and nesC, the current state of development tools for wireless sensor network still requires very low-level programming, which makes it hard for the developers to maintain a high-level view of the system operation. During the validation stage, lack of sophisticated debugging tools for sensor networks makes it difficult to make the connection between a high-level functional or performance requirement and a particular aspect of system implementation. This paper investigates a high-level approach to examine execution data from a simulator and analyze it using runtime verification. The technique 1) identifies and formally specifies high-level requirements for the system under development, 2) monitors a distributed wireless sensor network application using data provided by the simulator, and 3) checks for timing and dynamic properties to gain understanding of the relevant behaviors of wireless sensor nodes and to provide a systematic approach in finding bugs and errors. A particular runtime verification used inthis paper is MaC. MaC provides specification languages capable of expressing functional, timing, and probabilistic properties to specify requirements or patterns of errors. Properties can, for example, examine periodic behaviors or identify a faulty node. MaC then monitors and checks a wireless sensor network application against its specification by observing data produced by a simulator. The motivation for applying the monitoring and checking technique to check wireless sensor network applications is threefold: 1) raise the development level for wireless sensor network, 2) provide a mechanism for understanding high-level behaviors of the system in terms of low-level observation, and 3) provide a tool based on the acceptance of the state of the art development tool for sensor networks.
Cite as

Oleg Sokolsky, Usa Sammapun, John Regehr, and Insup Lee. Runtime Verification for Wireless Sensor Network Applications. In Runtime Verification. Dagstuhl Seminar Proceedings, Volume 7011, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{sokolsky_et_al:DagSemProc.07011.4,
  author =	{Sokolsky, Oleg and Sammapun, Usa and Regehr, John and Lee, Insup},
  title =	{{Runtime Verification for Wireless Sensor Network Applications}},
  booktitle =	{Runtime Verification},
  pages =	{1--9},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7011},
  editor =	{Bernd Finkbeiner and Klaus Havelund and Grigore Rosu and Oleg Sokolsky},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07011.4},
  URN =		{urn:nbn:de:0030-drops-13719},
  doi =		{10.4230/DagSemProc.07011.4},
  annote =	{Keywords: Runtime verification, wireless sensor network, Avrora simulator}
}

Filters

  • Authors
  • F
  • Finkbeiner, Bernd
  • H
  • Havelund, Klaus
  • L
  • Lee, Insup
  • R
  • Regehr, John
  • Rosu, Grigore
  • S
  • Sammapun, Usa
  • Sokolsky, Oleg
  • T
  • Tripakis, Stavros

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact