Specification and Validation of a Real-Time Simple Parallel Kernel for Dependable Distributed Systems

Software formal verification can provide guarantees regarding the implementation of complex software systems in respect to their specifications. Unfortunately, the practical applications of formal verification techniques are limited in case of modern systems. The operating system in particular, even though viewed as a critical component, has never been properly and formally evaluated in terms of provided functionality. In this we present and discuss such an experiment, based on a LOTOS specification, designed to evaluate a real-time UNIX-based parallel kernel. The purpose of this specification experiment is to evaluate the kernel using LOTOS and CADP tool box. Such instruments provide good capabilities to model and validate real-time features with realistic and complex industrial products. We present specification formal verification results validated using the CADP tool-box for a set of general properties referring the correctness of the kernel´s functionality. In the end we discuss limitations and future solutions and contributions of the formal verification domain to providing correctness guarantees for complex modern applications.