Formal verification of concurrent aspects in the design of a sensor web

This presentation reports on a project that verified some of the concurrent aspects of the design of SEAMONSTER, a smart sensor web project for environment data collection in the Lemon Creek watershed in Juneau, Alaska. Since concurrent systems can have many ways of interleaving the executions of subsystems, it is infeasible to test every possible scenario. The project, therefore, used a form of formal verification known as model checking, where a design is represented by a set of finite state automata (FSAs) and the specification is captured by statements in a temporal logic. The design is correct with respect to the specification if the set of FSAs is a model of the specification (i.e., provides an interpretation under which all specification statements are true). The SPIN software tool was used to model check properties of the design of SEQAMONSTER. Note that the FSAs are non-terminating and require the criterion for acceptance is changed to: in a (infinite) run, there must be infinitely many transitions into final states. SPIN uses the PROMELA language to build verification models. PROMELA does not contain all of the features of a full-featured programming language; its min constructs are processes, data objects, and message channels. The temporal logic used is Linear Temporal Logic (LTL). In LTL, one can encode formulae about the future of paths such as that a condition will eventually be true or that a condition will be true until another fact becomes true. LTL specifications are converted into to PROMELA code via the LTL parser and translator. SPIN can be used to simulate the PROMELA model and to verify the PROMELA model against the LTL specifications. This presentation outlines how this was done for a design that was reverse engineered from SEAMONSTER and for specifications expressing required behavior.

PRESENTATION TYPE: Oral

TECHNICAL AREA: Remote Sensing and Satellites

AFFILIATION (Pogue): STUDENT (Graduate)

CENTER AFFILIATION: NOAA-ISET

ARE YOU APPLYING FOR A STUDENT TRAVEL AWARD: NO