Real-Time Parallel Kernel for Dependable Distributed Systems

Organisation:	Polytechnic University of Bucharest (ROMANIA)
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Operating Systems.
Period:	2012
Size:	n/a.
Description:	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.
Conclusions:	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.
Publications:	[Ganea-Pop-Dobre-Cristea-12] 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
Contact:	Prof. dr. ing. Valentin Cristea Computer Science Department POLITEHNICA University of Bucharest 313 Splaiul Independentei, Sector 6 Bucharest 060042 Romania Tel: +40 21 4029194 Fax: +40 21 3181014 Email: Valentin.Cristea@cs.pub.ro
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page