Applying the B formal method to the Bossa domain-specific language

Domain-specific languages (DSLs) are used in both industry and research, in complex areas as varied as data mining [5], graphics [7], and device driver development [10]. A DSL provides high-level domain-specific abstractions that encapsulate domain expertise, thus making programming easier and less error-prone. Such languages also promise to be more amenable to verification, as the set of language abstractions can be designed to be easy to relate to desired properties and can be constrained to avoid problematic constructs such as unbounded loops. Nevertheless, many DSLs provide no verification, and those that do typically either rely on verification provided by a general-purpose host language or use ad hoc analyzers. The former approach is, however, limited to the facilities of the host language, which are rarely adequate for expressing and checking domain-specific properties, while the latter puts a huge burden on the DSL developer. We observe that many powerful verification systems have been developed in the formal methods community. Our goal is to realize the potential for verification of DSLs by harnessing these resources in designing and implementing DSL verifiers. To begin to bridge the gap between existing approaches to program verification and DSLs, we are applying the B formal method [1] to the Bossa DSL [9]. B is a refinementbased formal method that has been used for the development of safety critical software, especially in the domain of railway systems [2, 3]. The main feature of a B development process is that it proves that the final code implements its formal specification. Bossa is a DSL for specifying operating system (OS) kernel process scheduling policies. It has been implemented in the OSes Linux and Chorus. It has a formal semantics, and an ad hoc verifier that checks that a Bossa scheduling policy conforms to a model of the scheduling requirements of the target OS. This verifier is, however, hand-coded and complex, and thus hard to maintain as the language or set of desired properties evolves. Furthermore, it only checks the interaction between the scheduling policy and the OS, and is thus not suitable for checking properties of the implemented algorithm, such as liveness and fairness. In this paper, we show how B can be used to replace the ad hoc verifier of Bossa. We are currently working on extending this formal development to account for a wider range of properties. The rest of this paper is organized as follows. Section 2 provides an overview of Bossa. Section 3 gives a brief overview of the B method. Section 4 elaborates the B development of a Bossa specification and describes how 1 scheduler RM = { process = { time period; ... } states = { RUNNING running : process; 5 READY ready : select queue; READY yield : process; BLOCKED blocked : queue; BLOCKED computation_ended : queue; TERMINATED terminated; 10 } ordering_criteria = { lowest period }