Keynote
|
Heike Wehrheim (Paderborn University, Germany) gives the TAP keynote.
Extracting Unverified Program Parts from Software Verification Runs |
Abstract: Software verification tools automatically check for the absence of errors in programs. Not all verification runs do, however, manage to check all of the program’s real executions. Reasons might be that the program’s size or form of statements are beyond a verifier’s capabilities or that the verifier makes assumption about the executing processor which are in reality not satisfied. For completing such partial verification runs, techniques for extraction of unverified program parts are required. With such techniques at hand, the unverified parts could be given to a second validation tool, e.g. a tester. The talk will explain two such techniques for the extraction of unverified parts. The first aims at generating a residual program containing the unverified executions. Residual programs can then be passed to arbitrary other software validation tools. The second technique extracts conditions on hardware instructions which were assumed during verification. Such conditions can for instance be used to check whether software verification results are still valid on approximate hardware.
Short Bio: Heike Wehrheim is a full professor of Computer Science at Paderborn University, Germany. Before, she worked as a post-doc at the University of Oldenburg, obtained her PhD from Hildesheim University and studied at the University of Bonn. Her research interest are formal methods and software verification, in particular recently the combination of different verification techniques.
Invited Tutorial
|
Ana Cavalcanti (University of York, UK) gives the TAP invited tutorial.
RoboStar Technology - Testing in Robotics Using Process Algebra |
Abstract: In the design of robotic systems, often, state machines are drawn to convey overall ideas; they are used as a basis to program tool-specific simulations. The simulation code, written in general or proprietary programming languages, is, however, the only early account of the robotic system. In this talk, we present a modern approach to design that supports the automatic generation of simulation code that is guaranteed to be correct, and complements the use of simulation with model checking, theorem proving, and systematic testing. This approach, under development by the RoboStar group (https://www.cs.york.ac.uk/robostar/), uses two domain-specific languages: RoboChart and RoboSim. RoboChart includes a controlled subset of UML-like state machines, a customised component-model, and primitives to specify timed and probabilistic properties. RoboChart is an event-based notation for design; RoboSim [2] is a matching cycle-based diagrammatic notation for simulation. Both RoboChart and RoboSim can be used to generate automatically mathematical models written using the CSP process algebra and its extensions to deal with rich data types and time. In this tutorial, I present RoboChart and RoboSim, demonstrate RoboTool, the tool that can be used to generate CSP models automatically, and give an overview of the work that we have carried out on testing from CSP-based models.
Short Bio: Ana Cavalcanti is a Professor at the University of York, UK, and a Royal Academy of Engineering Chair in Emerging Technologies. Her current work is on Software Engineering for Robotics, with a leading role in the RoboStar group (https://www.cs.york.ac.uk/robostar/). From 2012 to 2017, she held a Royal Society - Wolfson Research Merit Award. In 2003, she was awarded a Royal Society Industry Fellowship to work with QinetiQ on formal methods. She has published more than 150 papers, and chaired the Programme Committee of various well-established international conferences. She has a long-term interest in refinement, safety-critical systems, object-orientation , concurrency, and real-time applications. She has played a major role in the design and formalisation of a state-rich process algebra, namely, Circus, and its development techniques using the Hoare and He’s Unifying Theories of Programming. She is currently Chair of the Formal Methods Europe association.