Title

Toward Formal Verification of Rule-Based Systems: A Shared Dataspace Perspective

Authors

H. Conrad Cunningham, Washington University in St. Louis
Gruia-Catalin Roman, Washington University in St. Louis

Document Type

Technical Report

Publication Date

1989-06-01

Filename

WUCS-89-28.pdf

DOI:

10.7936/K7B56H10

Technical Report Number

WUCS-89-28

Abstract

Rule-based programs used in mission- and safety-critical applications need to be shown to be free of hazards. This paper discusses formal proof-techniques which promise to assist designers in this task. In this paper we show that the shared dataspace language Swarm has many key features in common with rule-based languages. We outline an assertional programming logic for Swarm programs and use the logic to reason about the correctness of a simple program. This logic is a suitable foundation for the development of techniques specific to present and future rule-based languages.

Comments

Permanent URL: http://dx.doi.org/10.7936/K7B56H10

Recommended Citation

Cunningham, H. Conrad and Roman, Gruia-Catalin, "Toward Formal Verification of Rule-Based Systems: A Shared Dataspace Perspective" Report Number: WUCS-89-28 (1989). All Computer Science and Engineering Research.
https://openscholarship.wustl.edu/cse_research/741