Martin Wirsing, Ludwig-Maximilians-Universität München, Germany
A Component Framework for Simulation-Based Online Planning
in cooperation with Lenz Belzner and
Rolf Hennicker
Abstract. This work proposes a formal component framework for modeling and assessing autonomous systems operating in domains with large probabilistic state spaces and high branching factors. The framework defines components for acting and deliberation, and specifies their interactions. It comprises a mathematical description of specification requirements for autonomous systems. We discuss the role of such a specification in the context of simulation-based online planning. Moreover, an approach for relating goals given as bounded LTL formulae to utility functions driving autonomous system adaptation is discussed. The framework is illustrated with a robotic rescue example.
David Déharbe, Universidade Federal do Rio Grande do Norte, Brazil
A Formal Framework for the Design of Software Components with the B method
Abstract. B is a formal method used to design software components for safety-critical systems. The B method starts with the specification of the component as an abstract specification and proceeds by application of successive refinements until a detailed, algorithmic implementation has been derived. In all stages of the methods, the artifacts are subject to formal verification to ensure consistency.
We present a formalization framework for the B method based on Labelled Transition Systems (LTS) as semantics models. We establish the relationship between the generation of proof obligations mandated by the B method with the preservation of invariants in LTS, and between the notion of refinement in B and the concept of simulation in LTS. Finally we formalize, in this context, the concept of sound B development of a software component. All the formalization is expressed and machine-checked with Isabelle/HOL.
Renato Cerqueira, IBM Research, Brazil
Towards Pragmatic Contracts
Abstract. In this presentation, I will revisit some observations made during the last 20 years, while I was participating in R&D projects related to component-based development. I will focus on lessons learned and on how I ended up taking a path that tries to bring approaches and techniques from HCI to help in the design and evaluation of programmable interfaces.