Polytechnic University of Bucharest (ROMANIA)
CADP (Construction and Analysis of Distributed Processes)
Software formal verification can provide guarantees regarding the
implementation of complex software systems with respect to their
specifications. Unfortunately, the operating system, even though
viewed as a critical component, has never been properly and formally
evaluated in terms of provided functionality. Given that recent formal
methods and verification provide good capabilities to model and
validate real-time features with realistic and complex industrial
products, this work presents an experiment with the purpose of
evaluating a real-time UNIX-based parallel kernel.
The kernel operating system is intended to be suitable for real-time processing, possibly in an embedded context. This kernel should, in addition, be portable and, thus, there is no need to specify any interrupt service routines or the hardware clock and its associated driver. The kernel implements a priority based-scheduler, process abstraction, and inter-process communication (IPC) mechanisms. The storage is allocated statically, off-line, during kernel configuration. The kernel is statically linked with the user processes that run on it. This simple approach regards the kernel as a layered entity: a layer of primitives is defined to execute above the hardware, providing a collection of abstractions to be employed by the remainder of the system. The kernel was specified in LOTOS as a collection of parallel agents modelling the operating systems activities (scheduler, process table maintainer, context switcher, and IPC) interacting with the user processes. The resulting specification was analyzed using the CADP toolbox to check absence of deadlocks in different scenarios.
The kernel modeled in this study is a simple one, but still has a
complexity not far from that of the small kernels for embedded
real-time systems. If the kernel would be used in a real case,
additional features (device operations, clock process, preemption
management) will have to be modeled and implemented; however, this is
not particularly difficult because all necessary modules have already
been provided in the formal model. This study demonstrates the
possibility to define a formal model of a simple operating system and
to formally check some of its properties.
Octavian Ganea, Florin Pop, Ciprian Dobre, and Valentin Cristea.
"Specification and Validation of a Real-Time Simple Parallel Kernel
for Dependable Distributed Systems".
Proceedings of the 3rd International Conference on Emerging Intelligent
Data and Web Technologies EIDWT'2012 (Bucharest, Romania), IEEE
Press, September 2012.
Available on-line at: http://cipsm.hpc.pub.ro/Joomla/articles/2012_7.pdf
or from the CADP Web site in PDF or PostScript
Prof. dr. ing. Valentin Cristea
Computer Science Department
POLITEHNICA University of Bucharest
313 Splaiul Independentei, Sector 6
Tel: +40 21 4029194
Fax: +40 21 3181014
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|