2 Search Results for "Sammapun, Usa"

Document
Pearl/Brave New Idea
DOI: 10.4230/LIPIcs.ECOOP.2025.42
Contract Systems Need Domain-Specific Notations (Pearl/Brave New Idea)

Authors: Cameron Moy, Ryan Jung, and Matthias Felleisen

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Contract systems enable programmers to state specifications and have them enforced at run time. First-order contracts are expressed using ordinary code, while higher-order contracts are expressed using the notation familiar from type systems. Most interface descriptions, though, come with properties that involve not just assertions about single method calls, but entire call chains. Typical contract systems cannot express these specifications concisely. Such specifications demand domain-specific notations. In response, this paper proposes that contract systems abstract over the notation used for stating specifications. It presents an architecture for such a system, some illustrative examples, and an evaluation in terms of common notations from the literature.
Cite as

Cameron Moy, Ryan Jung, and Matthias Felleisen. Contract Systems Need Domain-Specific Notations (Pearl/Brave New Idea). In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 42:1-42:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{moy_et_al:LIPIcs.ECOOP.2025.42,
  author =	{Moy, Cameron and Jung, Ryan and Felleisen, Matthias},
  title =	{{Contract Systems Need Domain-Specific Notations}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{42:1--42:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.42},
  URN =		{urn:nbn:de:0030-drops-233348},
  doi =		{10.4230/LIPIcs.ECOOP.2025.42},
  annote =	{Keywords: software contracts, domain-specific languages}
}
Document
DOI: 10.4230/DagSemProc.07011.4
Runtime Verification for Wireless Sensor Network Applications

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

Published in: Dagstuhl Seminar Proceedings, Volume 7011, Runtime Verification (2008)

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}
}
  • Refine by Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2008

  • Refine by Author
  • 1 Felleisen, Matthias
  • 1 Jung, Ryan
  • 1 Lee, Insup
  • 1 Moy, Cameron
  • 1 Regehr, John
  • Show More...

  • Refine by Series/Journal
  • 1 LIPIcs
  • 1 DagSemProc

  • Refine by Classification
  • 1 Software and its engineering → Domain specific languages

  • Refine by Keyword
  • 1 Avrora simulator
  • 1 Runtime verification
  • 1 domain-specific languages
  • 1 software contracts
  • 1 wireless sensor network

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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