VSTTE 2018

Abstract: Model-based software development is a leading methodology for the construction of safety- and mission-critical embedded systems. Formal models of such systems can be validated, via formal verification or testing, against system-level requirements and modified as needed before the actual system is built. In many cases, source code can be even produced automatically from the model once the system designer is satisfied with it. As embedded systems become increasingly large and sophisticated the size and complexity of models grows correspondingly, making the verification of top-level requirements harder, especially in the case of infinite-state systems. We argue that, as with conventional software, contracts are an effective mechanism to establish boundaries between components in a system model, and can be used to aid the verification of system-level properties by using compositional reasoning techniques. Component-level contracts also enable formal analyses that provide more accurate feedback to identify sources of errors or the parts of a system that contribute to the satisfaction of a given requirement. This talk discusses our experience in designing an assume-guarantee-based contract language on top of the Lustre modeling language and leveraging it to extend the Kind 2 model checker with contract-based compositional reasoning techniques.

Abstract: Cesare Tinelli received a Ph.D. in Computer Science from the University of Illinois at Urbana-Champaign in 1999 and is currently a full professor in Computer Science at the University of Iowa. Professor Tinelli has done seminal work in automated reasoning, in particular in Satisfiability Modulo Theories (SMT), a field he helped establish through his research and service activities. His work has appeared in more than 80 refereed publications and has been funded both by governmental agencies (AFOSR, AFRL, DARPA, NASA, NSF, and ONR) and corporations (Intel, General Electric, Rockwell Collins, and United Technologies). He is a founder and coordinator of the SMT-LIB initiative, an international effort aimed at standardizing benchmarks and I/O formats for SMT solvers. He has led the development of the award winning Darwin theorem prover and the Kind 1 and Kind 2 model checkers which has found users in the avionics and automotive industries. He has co-led the development of the widely used and award winning CVC3 and CVC4 SMT solvers. He also co-leads the development of StarExec, a cross community web-based service for the comparative evaluation of logic solvers. He is an associate editor of the Journal of Automated Reasoning and a founder the SMT workshop series and the Midwest Verification Day series. He has served in the program committee of more than 70 automated reasoning and formal methods conferences and workshops, as well as the steering committee of CADE, ETAPS, FTP, FroCoS, IJCAR, and SMT. He was the PC chair of FroCoS'11 and a PC co-chair of TACAS'15.

Abstract: Continual innovation of software verification theories & tools is essential in order to meet the challenges of ever-more complex software-intensive systems. But achieving impact ultimately requires an understanding of the engineering context in which the tools will be deployed. Based on our tried-and-trusted methods of high-integrity software development at Altran, I will identify key features of the industrial landscape in which software verification tools have to operate, and some of the pitfalls that can stop them being adopted, including regulation, qualification, scalability, cost justification, and the overall tool ecosystem. Within this context I will present Altran's own on-going research & development activities in verified software technologies. The talk will conclude by drawing some key lessons that can be applied to avoid the traps and pitfalls that tools encounter on their journey to succesful deployment.

Bio: Stuart Matthews has over 20 years' experience with high integrity software engineering including the application of formal methods for verification and validation of critical systems. Stuart is currently the head of R&T within the Intelligent Systems Expertise Centre at Altran UK with responsibility for the technology pipeline and a portfolio of on-going research projects. The portfolio includes the SPARK static verification toolset & support services for which Stuart also acts as the product manager at Altran.

Abstract: The increasing application of formal methods to the design of autonomous systems often requires extending the existing specification and modeling formalisms, and addressing new challenges for formal verification and synthesis. In this talk, I will focus on the application of reactive synthesis to the problem of automatically deriving strategies for autonomous mobile sensors conducting surveillance, that is, maintaining knowledge of the location of a moving, possibly adversarial target. By extending linear temporal logic with atomic surveillance predicates, complex temporal surveillance objectives can be formally specified in a way that allows for seamless combination with other task specifications. I will discuss two key challenges for applying state-of-the-art methods for reactive synthesis to temporal surveillance specifications. First, naively keeping track of the knowledge of the surveillance agent leads to a state-space explosion. Second, while sensor networks with a large number of dynamic sensors can achieve better coverage, synthesizing coordinated surveillance strategies is challenging computationally. I will outline how abstraction, refinement, and compositional synthesis techniques can be used to address these challenges.

Bio: Rayna Dimitrova is a Lecturer (Assistant Professor) at the University of Leicester, UK. Prior to that, she held postdoctoral positions at the University of Texas at Austin, and at the Max Planck Institute for Software Systems in Germany. She completed her PhD at Saarland University in Germany. Rayna's research is focused on the specification, verification, and synthesis of reactive systems. She primarily investigates quantitative versions of these questions, centered around the aspect of uncertainty in system and environment models. She is particularly interested in applications of formal methods to autonomous systems, where her work addresses the limitations faced by autonomous control due to imperfect sensing and stochastic disturbances.