Search

Critical (software) systems are all around us. These systems are typically characterised by stringent dependability requirements and demand elevated levels of robustness and fault tolerance. To assure that they function as intended and provide a number of quality guarantees, formal methods and automated verification techniques and tools have been in use in the engineering of such critical systems for many years now. In this introduction to the special issue FMICS-AVoCS on “Formal Methods and Automated Verification of Critical Systems”, we outline a number of recent achievements concerning the use of formal methods and automated verification techniques and tools for the specification and analysis of critical systems from a variety of application domains. These achievements are represented by six selected papers: five were selected from the joint 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems (FMICS-AVoCS 2016), while one of them was selected after an open call for papers. [ABSTRACT FROM AUTHOR]

Automated verification of operating system kernels is a challenging problem, partly due to the use of shared mutable data structures. In this paper, we show how we can automatically verify memory safety and functional correctness properties of the task scheduler component of the FreeRTOS kernel using the verification system Hip/Sleek. We show how some of Hip/Sleek features such as user-defined predicates and lemmas make the specifications highly expressive and the verification process viable. To the best of our knowledge, this is the first code-level verification of memory safety and functional correctness properties of the FreeRTOS scheduler. The outcome of our experiment confirms that Hip/Sleek can indeed be used to verify code that is used in production. Moreover, since the properties that we verify are quite general, we envisage that the same approach can be adopted to verify components of other operating systems. [ABSTRACT FROM AUTHOR]

Managing access control policies in modern computer systems can be challenging and error-prone. Combining multiple disparate access policies can introduce unintended consequences. In this paper, we present a formal model for specifying access to resources, a model that encompasses the semantics of the xacml access control language. From this model we define several ordering relations on access control policies that can be used to automatically verify properties of the policies. We present a tool for automatically verifying these properties by translating these ordering relations to Boolean satisfiability problems and then applying a sat solver. Our experimental results demonstrate that automated verification of xacml policies is feasible using this approach. [ABSTRACT FROM AUTHOR]