Representing the Unknown in Specification Languages

Abstract

During the operation of software-controlled physical system, there are times when the values of environmental variables are not known by the control software. To correctly specify and reason about such systems, a specification language must allow variables to take a special undefined value that signifies that the value of the variable is unknown. Adding an undefined value to the type system of a language, however, complicates the semantics of the language because it causes many of the arithmetic operators to become partial functions. In this paper we discuss different approaches to managing undefined values and present our approach for the specification language RSML-e. We provide a loose semantics that allows simulation/execution of incomplete models, and a tight semantics, which, given a completed model, is used for code-generation and static analysis. To prevent misuse of undefined values, we present a test that ensures that predicates in RSML-e cannot evaluate to undefined, and that variables cannot implicitly take on undefined values.