Keynote Speaker :: SETECEC 2012

 Abstract

Application of Verification Techniques to Safety and Security

In this keynote, I give an overview of the state of the art of formal verification techniques to the engineering of safe and secure systems. The main focus is on the support with mechanized verification techniques, in particular modelchecking. The first case study is on the formal modeling and verification of the safety critical elevator system TWIN of ThyssenKrupp. This system operates two cabins in one shaft with the potential of collision. A simple and successful safety analysis with the modelchecking system SMV is demonstrated. The second case study ventures into the rising field of social engineering attacks on security. We consider the security analysis of an insider attack illustrating the benefits of modelchecking with belief logics and actor system modeling.