Towards model checking with java pathfinder for autonomic systems specified and generated with ASSL

Emil Vassev, Mike Hinchey, Aaron Quigley

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

Autonomic computing has been recognized as a valid approach to the development of large-scale self-managing complex systems. The Autonomic System Specification Language (ASSL) is an initiative for the development of autonomic systems where we approach the problem of formal specification, validation, and code generation of such systems within a framework. As part of our research on ASSL, we have developed and investigated different approaches to software verification. Currently, the latter is possible via built-in consistency checking and functional testing where handling logical errors is a daunting task. In this paper, we discuss our work on model checking with NASA's Java PathFinder tool, which is an explicit-state model checker that works directly on the generated Java code. We propose optional automatic generation of test drivers in the form of PathFinder API calls seeded in the ASSL-generated code.

Original languageEnglish
Title of host publicationICSOFT 2009 - 4th International Conference on Software and Data Technologies, Proceedings
Pages251-256
Number of pages6
Publication statusPublished - 2009
EventICSOFT 2009 - 4th International Conference on Software and Data Technologies - Sofia, Bulgaria
Duration: 26 Jul 200929 Jul 2009

Publication series

NameICSOFT 2009 - 4th International Conference on Software and Data Technologies, Proceedings
Volume1

Conference

ConferenceICSOFT 2009 - 4th International Conference on Software and Data Technologies
Country/TerritoryBulgaria
CitySofia
Period26/07/0929/07/09

Keywords

  • ASSL
  • Autonomic computing
  • Java pathfinder
  • Model checking

Fingerprint

Dive into the research topics of 'Towards model checking with java pathfinder for autonomic systems specified and generated with ASSL'. Together they form a unique fingerprint.

Cite this