Reflective specification: applying a reflective language to formal specification

This paper reports on a technique for specifying concurrent systems by using a formal specification language with reflective computation mechanism. We call the specifications written by a reflective language reflective specifications. Our reflective language is an enhanced version of LOTOS (Language of Temporal Ordering Specification). We embedded reflection or reflective computation facilities to behaviour specification part of LOTOS in order to define complex behaviour in a simple and natural way. Reflection in a program is a mechanism to access and modify its execution states which its executor has. Our enhanced version of LOTOS is called RLOTOS, and has two level architecture - object level and meta level. The processes in the meta level, called meta processes, have the computational information and interpret the behaviour expressions of their object level processes. We can define meta processes in the same manner as LOTOS processes to control the behaviour of the object level processes. In this paper, we present a case study of specifying an operating system by using RLOTOS. Furthermore we discuss the method to construct comprehensive formal specifications by using reflective languages and explore the applicability of the reflective language to formal specification. The essential point of comprehensiveness is that the meta properties of the system such as control characteristics can be specified separately from the object level properties.