How should we build that? Evolving a development environment that's suitable for constructing today's systems
We are building ever more complex systems, and demanding of them ever higher standards of reliability, functionality, and safety. The development environment for the successful project you just delivered almost certainly needs enhancing for your next project. Maybe your team needs to use new tools, new methodologies, new architectural patterns, new process, or just a new language. You can analyse past projects, and research other people's work, but how do you choose what enhancements to make? And how do you deploy new process or tooling in an industrial context where time-to-market, margin, and success are everything? This talk will look at the key drivers behind the successful adoption of any new process or tool - from a small incremental update to a major shift in development philosophy. Along the way we will look at some real-world successes, and face up to a few challenges. About the speaker:
Neil is the Head of Capability for Altran UK. He has worked in the area of bespoke safety-critical software for over 15 years. In that time he has delivered signature projects into a variant of markets, including UK Air Traffic Control, Aerospace, Defence, and Finance. His projects have included the first deployments to new regulatory standards, and the industrial introduction of new technologies. He is currently interested in the sustainable evolution required to keep hi-tec companies at the forefront of their markets.
Engineering Multi-View Models for Model-Driven Engineering
The effectiveness of model-driven engineering relies on our ability to build high-quality models. This task is intrinsically difficult. We need to produce sufficiently complete, adequate, consistent, and well-structured models from incomplete, imprecise, and sparse material originating from multiple, often conflicting sources. The systems we need to consider generally comprises software components, devices and people.
Such models should integrate the intentional, structural, functional, and behavioral facets of the system being developed. Rigorous techniques are needed for model construction, analysis, and evolution. Such techniques should support early and incremental reasoning about partial models for a variety of purposes, including goal satisfaction arguments; property checks; model animations; the evaluation of alternative system design options; the systematic identification and resolution of risks, threats and conflicts; and traceability management.
The tension between technical precision and practical applicability calls for a suitable mix of heuristic, deductive, and inductive forms of reasoning on a suitable mix of declarative and operational models. Formal techniques should be deployed only when and where needed, and kept hidden wherever possible.
The talk will provide a retrospective account of our research efforts and practical experience along this route, including recent progress in model engineering for safety-critical human-intensive systems. About the speaker:
Axel van Lamsweerde is Full Professor at the Department of Computing Science of the Université catholique de Louvain, Belgium. His research interests are in precise techniques for requirements engineering, system modeling, high assurance systems, lightweight formal methods, process modeling and analysis, medical safety, and knowledge-based software development environments. Since 1990 he has been instrumental in the development of the KAOS goal-oriented modeling language, method, and toolset. He is author of the book "Requirements engineering: From System Goals to UML Models to Software Specifications" (Wiley). He was Editor-in-Chief of the ACM Transactions in Software Engineering and Methodology, Program Chair of major international software engineering conferences including ESEC'91 and ICSE'94, and Associate Editor of the IEEE Transactions on Software Engineering. He is an ACM Fellow (2000), recipient of the ACM SIGSOFT Distinguished Service Award (2003), and the ACM SIGSOFT Outstanding Research Award (2008).
Model Repair for Markov Decision Processes
Markov decision processes (MDPs) are often used for modelling distributed systems with probabilistic failure or randomisation. We consider the problem of model repair for MDPs defined as follows: if the MDP fails to satisfy a property, we aim to find new values for the transition probabilities so that the property is guaranteed to hold, while at the same time the cost of repair is minimised. Because solving the MDP repair problem exactly is infeasible, in this paper we focus on approximate solution methods. We first formulate a region-based approach, which yields an interval in which the minimal repair cost is contained. As an alternative, we also consider sampling-based approaches, which are faster but unable to provide lower bounds on the repair cost. We have integrated both methods into the probabilistic model checker PRISM and demonstrated their usefulness in practice using a computer virus case study.
About the speaker:
Marta Kwiatkowska is Professor of Computing Systems and Fellow of Trinity College, University of Oxford. She was elected to Academia Europea in 2011 and received a prestigious ERC Advanced Grant VERIWARE "From software verification to everyware verification", 2010-15.
Kwiatkowska's research is concerned with modelling and automated verification techniques for probabilistic systems, with application to engineered and biological systems. She gave the 2012 Milner lecture awarded for “excellent and original theoretical work which has a perceived significance for practical computing”. The PRISM model checker (www.prismmodelchecker.org) developed under her leadership is internationally leading in the area and widely used for research and teaching. Applications of probabilistic model checking have spanned communication and security protocols, nanotechnology designs, power management, planning, systems biology and DNA computation. Her research is supported by funding from EPSRC, EU, Oxford Martin School and Microsoft Research.
Marta Kwiatkowska serves on numerous programme committees and editorial boards of several journals, including IEEE Transactions on Software Engineering, Formal Methods in System Design and Royal Society's Philosophical Transactions A. She was lead organiser of the Royal Society Discussion Meeting "From computers to ubiquitous computing, by 2020" and guest co-editor of the associated Proceedings in Phil. Trans. R. Soc. A vol 366 no 1881.