Search

In real-time systems with threads, resource locking and priority scheduling, one faces the problem of Priority Inversion. This problem can make the behaviour of threads unpredictable and the resulting bugs can be hard to find. The Priority Inheritance Protocol is one solution implemented in many systems for solving this problem, but the correctness of this solution has never been formally verified in a theorem prover. As already pointed out in the literature, the original informal investigation of the Property Inheritance Protocol presents a correctness “proof” for an incorrect algorithm. In this paper we fix the problem of this proof by making all notions precise and implementing a variant of a solution proposed earlier. We also generalise the scheduling problem to the practically relevant case where crit- ical sections can overlap. Our formalisation in Isabelle/HOL is based on Paulson’s inductive approach to protocol verification. The formalisation not only uncovers facts overlooked in the literature, but also helps with an efficient implementation of this protocol. Earlier imple- mentations were criticised as too inefficient. Our implementation builds on top of the small PINTOS operating system used for teaching.

AlN chlorination route, in the present work, was proposed to extract Aluminum from aluminum nitride under vacuum. Density functional theory (DFT) were implemented to study the interaction of AlCl 3 molecule and AlN ( 10 1 ¯ 0 ) surface. The results of DFT indicate that chemisorbed AlCl 3 adsorption configuration was observed on the clean AlN ( 10 1 ¯ 0 ) surface after structure optimization, and adsorbed AlCl molecules were generated after 1 ps dynamic simulation time. The phase and composition of condensate were examined by means of XRD and EDS. It was found that 97.76 wt% of Al metal was obtained in the experiment B (in the presence of AlCl 3 ), however, no condensate was collected in the experiment A (without AlCl 3 ) at 1760 K under pressure of average 60 Pa. The results show that AlN chlorination route is an alternative Al production method from aluminum nitride.

There are numerous textbooks on regular languages. Many of them focus on finite automata for proving properties. Unfortunately, automata are not so straightforward to formalise in theorem provers. The reason is that natural representations for automata are graphs, matrices or functions, none of which are inductive datatypes. Regular expressions can be defined straightforwardly as a datatype and a corresponding reasoning infrastructure comes for free in theorem provers. We show in this paper that a central result from formal language theory--the Myhill-Nerode Theorem--can be recreated using only regular expressions. From this theorem many closure properties of regular languages follow.

If an access control policy promises that a resource is protected in a system, how do we know it is really protected? To give an answer we formalise in this paper the Role-Compatibility Model–a framework, introduced by Ott, in which access control policies can be expressed. We also give a dynamic model determining which security related events can happen while a system is running. We prove that if a policy in this framework ensures a resource is protected, then there is really no sequence of events that would compromise the security of this resource. We also prove the opposite: if a policy does not prevent a security compromise of a resource, then there is a sequence of events that will compromise it. Consequently, a static policy check is sufficient (sound and complete) in order to guarantee or expose the security of resources before running the system. Our formal model and correctness proof are mechanised in the Isabelle/HOL theorem prover using Paulson's inductive method for reasoning about valid sequences of events. Our results apply to the Role-Compatibility Model, but can be readily adapted to other role-based access control models.

Directory Service is used widely in modern communication networks. In this paper, we proposed and implemented a management system based on event bus pattern to manage directory service network constructed by improving OpenLDAP [1]. The management system presents good architecture while implementing complex management functions. The principles and use of event bus pattern in the system is described in detail and experience shows that this pattern makes the system have considerable flexibility, maintainability, extensibility and a general applicability to many other applications.