This year, STAF is proud to feature the following outstanding keynote speakers:
- Ramon Schiffelers: Empowering high tech systems engineering using MDSE ecosystems
- Georg Gottlob: General and Fractional Hypertree Decompositions: Hard and Easy Cases
- Lionel C. Briand: Model-driven verification and testing of cyber-physical systems: Tackling Scalability and Practicality Challenges
- Reiner Hähnle: Abstraction Refinement for the Analysis of Software Product Lines
Moreover, we are proud to feature an industry talk:
- Dennis Klassen, itemis: Requirements for Traceability and Test Coverage in German Common Criteria Schema
Empowering high tech systems engineering using MDSE ecosystems
Ramon Schiffelers, ASML, NL
Ramon Schiffelers is a software architect at ASML, world’s leading provider of lithography systems for the semiconductor industry, and assistant professor at the department of Mathematics and Computer Science at the Eindhoven University of Technology.
Within ASML, he is leading a research group (+/ 20 fte) consisting of (SW) architects, scientific programmers, (academic) researchers, and PhD, PDEng, and MSc students. Together with this group, he combines state-of-the-art methods and techniques from academia with state-of-the-practice in industry into so-called multi-disciplinary system engineering (MDSE) ecosystems. These ecosystems empower their users to develop complex, large-scale, software intensive systems.
Such (domain specific) ecosystems integrate:
- domain formalizations in terms of domain specific languages (DSLs),
- aspect models and tools for rigorous analysis and synthesis,
- automated model re-constructors and model inference algorithms to deal with legacy software components
He has successfully introduced several MDSE ecosystems in the development process and products of ASML.
General and Fractional Hypertree Decompositions: Hard and Easy Cases
Georg Gottlob, University of Oxford, UK
the more powerful generalized hypertree decompositions (GHDs), and the
yet more general fractional hypertree decompositions (FHD) are hypergraph decomposition
methods successfully used for answering conjunctive queries and for
solving constraint satisfaction problems. Each hypergraph H
has a width relative to each of these methods: its hypertree width
hw(H), its generalized hypertree width ghw(H), and its fractional
hypertree width fhw(H), respectively. While hw(H) ≤k can be checked in
polynomial time, the complexity of checking whether fhw(H) ≤k holds for a
fixed constant k was unknown. We settle this problem by proving that
checking whether fhw(H) ≤k is NP-complete, even for k=2 and by same
construction also the problem deciding whether ghw(H) ≤k is NP-complete
for k≥2. Hardness was previously known for k≥3, whilst the case k=2 has
remained open since 2001.
Given these hardness results, we investigate meaningful restrictions, for which checking for bounded ghw is easy. We study classes of hypergraphs that enjoy the bounded edge-intersection property (BIP) and the more general bounded multi-edge intersection property (BMIP). For such classes, for each constant k, checking whether ghw(H) ≤k, and if so, computing a GHD of width k of H is tractable and actually FPT. Finally we derive some approximability results for fhw. We consider classes of hypergraphs whose fhw is bounded by a constant k and which also enjoy the BIP or MIP, or bounded VC-dimension. For each hypergraph in such a class, we are able to compute an FHD of width O(k log k) efficiently. A different restriction on classes of hypergraphs gives a linear approximation in PTIME. Hypergraphs of bounded rank are a simple example of such a class. Joint work with Wolfgang Fischl and Reingard Pichler.
Georg Gottlob is a Professor of Informatics at Oxford University, a Fellow of St John’s College, Oxford, and an Adjunct Professor at TU Wien. His interests include AI, knowledge representation, logic and complexity, web data extraction, database theory, graph decomposition techniques. Gottlob is an ACM Fellow, an ECCAI Fellow, a Fellow of the Royal Society, and a member of the Austrian Academy of Sciences, the German National Academy of Sciences, and the Academia Europaea. He chaired the Program Committees of IJCAI 2003 and ACM PODS 2000, was the Editor in Chief of the Journal Artificial Intelligence Communications, and is currently a member of the editorial boards of journals, such as JACM and the Journal of Computer and System Sciences. Gottlob was awarded an ERC Advanced Investigator’s Grant for the project “DIADEM: Domain-centric Intelligent Automated Data Extraction Methodology” (see also http://diadem.cs.ox.ac.uk/).
Model-driven verification and testing of cyber-physical systems: Tackling Scalability and Practicality Challenges
Lionel Briand, University of Luxembourg, LU
This talk will report on various research collaboration projects with industry and the lessons learned we drew regarding the verification and testing of cyber-physical systems. Specific issues related to the uncertainty and dynamic behaviour of such systems will be addressed.
Novel and general solutions will be presented for Model-In-the-Loop (MIL) testing — a common practice in the embedded software industry — and results from Simulink and timed automata models in the automotive domain will be presented. Beyond this scope, more complex situations will be considered and future research plans will be outlined.
Lionel Briand is professor and FNR PEARL chair in software verification and validation at the SnT centre for Security, Reliability, and Trust, University of Luxembourg. He also acts as vice-director of the centre. Lionel started his career as a software engineer in France (CS Communications & Systems) and has conducted applied research in collaboration with industry for more than 22 years.
Until moving to Luxembourg in January 2012, he was heading the Certus center for software verification and validation at Simula Research Laboratory, where he was leading applied research projects in collaboration with industrial partners. Before that, he was on the faculty of the department of Systems and Computer Engineering, Carleton University, Ottawa, Canada, where he was full professor and held the Canada Research Chair (Tier I) in Software Quality Engineering. He has also been the software quality engineering department head at the Fraunhofer Institute for Experimental Software Engineering, Germany, and worked as a research scientist for the Software Engineering Laboratory, a consortium of the NASA Goddard Space Flight Center, CSC, and the University of Maryland, USA.
Lionel has been on the program, steering, or organization committees of many international, IEEE and ACM conferences. He is the coeditor-in-chief of Empirical Software Engineering (Springer) and is a member of the editorial boards of Systems and Software Modeling (Springer) and Software Testing, Verification, and Reliability (Wiley). He was on the board of IEEE Transactions on Software Engineering from 2000 to 2004.
Lionel was elevated to the grade of IEEE Fellow in 2010 for his work on the testing of object-oriented systems. He was granted the IEEE Computer Society Harlan Mills award and the IEEE Reliability Society engineer-of-the-year award for his work on model-based verification and testing, respectively in 2012 and 2014. His research interests include: software testing and verification, model-driven software development, search-based software engineering, and empirical software engineering.
Abstraction Refinement for the Analysis of Software Product Lines
Reiner Hähnle, Technical University of Darmstadt, DE
We generalize the principle of counter example-guided data abstraction refinement (CEGAR) to guided refinement of Software Product Lines (SPL) and of analysis tools. We also add a problem decomposition step. The result is a framework for formal SPL analysis via guided refinement and divide-and-conquer, through sound orchestration of multiple tools.
Reiner Hähnle received a Diploma and a Ph.D. in Computer Science from University of Karlsruhe and a Habilitation from Technical University of Vienna. From 2000 he was Associate Professor and from 2002 Full Professor of Computer Science at Chalmers University. Since 2011 he holds the Chair of Software Engineering at Technical University Darmstadt. He worked as a guest researcher at ICOT Tokyo, University of Tübingen, University of Turin, and University of Oslo. He authored and edited 180 international, peer-reviewed publications and served on 100 programme committees. Reiner was one of the founders of the Tableaux conference, a founding trustee of FLoC Inc., PC Chair of IJCAR, Tableaux, and TAP, as well as Wine Chair of ECOOP. His research interests include formal analysis and verification of OO languages, executable software models, tool-assisted debugging, test generation. Reiner is founder of the KeY verification system for Java and a co-designer of the executable modeling language ABS.
Requirements for Traceability and Test Coverage in German Common Criteria Schema
Industry Talk on Wednesday, July 19, 13:15 – 14:00
In the age of global digitalisation and IoT, the need for more security increases day by day. More and more organizations receive a request from the government to certify products according to technical requirements or the Common Criteria (CC) by the BSI. The German certification process for CC as well as the high effort for test development and documentation present a problem especially for newcomers. In addition to the necessary CC-specific documentation, the security functional requirements (sfr) need to be treated differently than the usual functional requirements. Thus the traceability of the sfr’s from the protection profile (pp) up to the test results is a challenge. In this presentation, we will show the CC process with possible occurring bottlenecks and discuss possible solutions for developers. One solution can be e.g. a requirements traceability tool with partial or full test case generation. The first problem to solve is the acceptance of the tool by the BSI. Furthermore we will share our experience in this specific discipline. This task takes a lot of know how in different domains, like domain specific knowledge about target of evaluation (toe), test suite development, requirement engineering and common criteria evaluation.