Introduction:
Development of integrated mixed-criticality systems is becoming increasingly popular for
application-specific systems, which needs separation mechanism for available onboard resources and the processors
equipped with hardware virtualization. Hardware virtualization allow the partitions to physical resources, which include
processor cores, memory, and I/O devices, among guest virtual machines (VMs). For building mixed criticality computing
environment, traditional virtual machine systems are inappropriate because they use hypervisors to schedule separate VMs
on physical processor cores. In this article, we discuss the design of an environment for mixed-criticality systems: The
Muen an x86/64 separation kernel for high assurance. The Muen Separation Kernel is an Open Source microkernel which
has no runtime errors at the source code level. The Muen separation kernel has been designed precisely to encounter the
challenging requirements of high-assurance systems built on the Intel x86/64 platform. Muen is under active development,
and none of the kernel properties of it has been verified yet. In this paper, we present a novel work of verifying one of the
kernel properties formally.
Method:
The CTL used in NuSMV is a first-order modal along with data-depended processes and regular formulas. CTL
is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined;
there are different paths in the future, any one of which might be an actual path that is realized . This section shows the
verification of all the requirements mentioned in section 3. In NuSMV tool the command used for verification of the
formulas written in CTL is checkctlspec -p ”CTL-expression”. The nearest quantifier binds each occurrence of a variable
in the scope of the bound variable, which has the same name and the same number of arguments.
Result:
Formal methods have been applied to various projects for specification and verification purpose. Some of them
are the SCOMP , SeaView , LOCK,and Multinet Gateway projects. The TLS was written formally. Several mappings
were done between the TLS and the SCOMP code: Informal English language to TLS, TLS to actual code , and TLS to
pseudo-code. The authors present an ACL2 model for a generic separation kernel also known as GWV approach.
Conclusion:
We consider the formal verification of data separation property which is one of the crucial modules to
achieve the separation functionality. The verification of the data separation manager is carried out on the design level
using the NuSMV tool. Furthermore, we present the complete model of the data separation unit along with its code written
in the NuSMV modelling language. Finally, we have converted the non-functional requirements into the formal logic,
which then has verified the model formally.
A Virtualized Separation Kernel for Mixed-Criticality Systems
