3rd International Workshop on Explainability of Real-time Systems and their Analysis at the IEEE Real-Time Systems Symposium (RTSS 2024) in York, UK
Today, almost all verification techniques provide answers to questions but do not provide explanations. We will address that.
Important dates
•Submission deadline:
September 6, 2024
September 13, 2024
• Notification of acceptance:
October 4, 2024
October 7, 2024
• Final version due:
October 21, 2024
• Workshop:
December 10, 2024
Program Chairs
Bjorn Andersson,
SEI/CMU, USA
Philippa Ryan,
UYork, UK
Program Committee
Ademola (Peter) Adejokun,
Lockheed Martin, USA
Ahlem Mifdaoui,
UToulouse, FR
Al Mok,
UTexas, USA
Andrew Banks,
LDRA, UK
C. Michael Holloway,
NASA, USA
Chi-Sheng (Daniel) Shih,
NTU, TW
Dionisio de Niz,
SEI/CMU, USA
Elena Troubitsyna,
KTH, SE
Ganesh Pai,
KBR/NASA ARC, USA
George Romanski,
FAA, USA
Guillem Bernat,
Rapita, UK
Hyoseung Kim,
UCR, USA
Isaac Amundson,
Collins Aerospace, USA
Jie Zou,
UYork, UK
John Lehoczky,
CMU, USA
Mallory Graydon,
NASA, USA
Mark Klein,
SEI/CMU, USA
Rafael Zalman,
Infineon, DE
Shige Wang,
Motional, USA
Program
Location: Room Minster Room. Details from RTSS about the venue are here.
Link to workshop proceeding is here.
09:00am Welcome
Bjorn Andersson
09:05am Keynote 1
Session chair: Iain Bate
Andrew Banks, "The C Language… you wouldn’t start from here!"
LDRA
10:10am Retrospective of earlier ERSA
Bjorn Andersson
10:15am Coffee break
10:45am Peer-reviewed papers
Session chair: Bjorn Andersson
Reinhard Wilhelm and Jan Reineke, "Sound WCET Analysis, Explanation of the Method and of the Results"
Isaac Amundson, Amer Tahat, David Hardin, and Darren Cofer, "Towards Explainable Compositional Reasoning"
Leo Bishop and Leandro Soares Indrusiak, "Strengthening Real-Time Analysis by Evolving Counterexamples"
11:59am Lunch
01:00pm Keynote 2
Session chair: Bjorn Andersson
Speaker: Matt Osborne (Independent Safety Consultant)
02:00pm Panel: Role of LLM in certification and the assurance tool chain
Session chair: Iain Bate
Panelists:
Bjorn Andersson
Kester Clegg
Leandro Soares Indrusiak
Will Klieber
02:45pm Adjourn
About the keynote speakers
Andrew Banks: a lead/principal systems- and software-engineering professional, specializing in real-time/embedded systems, their assurance and their approvals.
With over 30 years of experience directing, managing and leading safety critical software/systems development across the aerospace, defence, automotive, and medical domains, I'm now poacher turned gamekeeper and am working for tool-vendor LDRA, and helping to guide client companies achieve their certifications and approvals.
In addition, currently Chairman of the MISRA C Working Group, the UK Head of Delegation to ISO/IEC JTC1/SC7 "Software & Systems Engineering", Chairman of the BSI Software Testing Working Group, a member of the ISO and BSI C language panels and contributor to several other software- and systems-engineering groups.
As well as being technically focused, I'm also a strong advocate of Continued Professional Development, and of encouraging all engineers to gain Professional Accreditation - as such, I'm a Mentor for both the BCS and the IET.
Personally I am honoured to have been awarded IEng MIET FBCS CITP MInstLM FRSA, and am a Freeman of the Worshipful Company of Information Technologists (WCIT).
Matt Osborne: is an Independent Safety Consultant and a Visiting Research Fellow within the Centre for Assuring Autonomy, in the Department of Computer Science, at the University of York. As a Safety Scientist who espouses the values of reality-based safety science, his research interests are:
Supporting Software Safety Assurance
The Safety of Decision-Making in Autonomy
The Safety of Software in the ML Stack
Having his feet firmly placed in both engineering practice and academia, Matt is able to promote, facilitate, engender, and uphold the required commitments for Reality-Based Safety Science.
Matt is The Furious Engineer. - www.thefuriousengineer.com
Paper submission
Workshop website: https://sites.google.com/view/ersa24
Format: Extended abstract or position papers to define the area, up to 4 pages, IEEE Manuscript Template Conference Proceedings
Online submission: https://easychair.org/conferences/?conf=ersa24
Motivation, Goal, and Topics
Background: Many software-intensive systems of current and future application domains require (or will require) approval from a certification authority before being deployed. Approval will hinge on presentation of certification evidence about software design and performance. Examples of application domains include: aircraft, medical devices, spacecraft, autonomous ground vehicles, autonomous air vehicles. Examples of current certification authorities include: Federal Aviation Administration, European Union Aviation Safety Agency, Food and Drug Administration, Office for Nuclear Regulation.
Current pain: Today, each established application domain has a set of guidance documents. These tend to be process-oriented; i.e., (i) prescribe specific techniques for analyzing, testing and developing software, (ii) prescribe how the applicant should present data to the certification authority, (iii) state high-level objectives, and (iv) state pitfalls and approaches that should be avoided. This mindset has been successful in many domains. For example, among US air carriers, the safety record today is much better than it was decades ago. Unfortunately, the approach also has some limitations including: (i) slow adoption of new techniques (ii) lack of applicability to future technology (e.g., AI) (iii) difficulties scaling to complex software and hardware (e.g., multi-core), (iv) cost and effort to maintain certification evidence is prohibitive for frequent and late changes, (v) emphasis is on applying processes (tickbox) rather than focusing on direct evidence of the safety of the software. Thus developers are unable to take full advantage of the research within the real-time systems community including recent knowledge, techniques, advances and references to papers. One key barrier is presenting the strengths, weaknesses and applicability of recent research to certification authorities and other stakeholders. This includes explaining the methods and their results to non-specialists. Thus, it is worth exploring alternatives, specifically (i) whether explainability can help, (ii) what explainability means, and (iii) how it can be achieved for real-time systems.
Goal: The goal is to understand the role, meaning, and value of explanation in critical systems—in particular real-time systems.
Past Edition: https://sites.google.com/view/ersa22, https://sites.google.com/view/ersa23
Non-Exhaustive List of Topics:
Things needing explanation (e.g., output of schedulability or WCET analysis, post-mortem/close-call trace)
Ways of explaining: Examples (e.g., Gantt chart of a schedule); Proofs (e.g., trees, unsat core); Models (as in a satisfiable assignment)
Representations of explanations: Graphical (pictures); Textual; Anthropomorphizing (min-max or forall exist can be viewed as a game); Analogies
Building explanation from output from existing tool (e.g., from a proof that is a sequence of lemmas, for each lemma generate a picture)
Performance metrics of explanation (e.g., human skill and/or effort needed to understand the explanation)
Points in a software development life cycle and persons to which explainability are most valuable
Change in certification guidance documents needed for value of explainability to accrue
Tool qualification of explainability methods
Using ideas from theoretical computer science
Computational complexity issues regarding explainability (size of certificate, size of explanation related to explanation of a property versus explanation of the negation of a property, problem and its complementary problem, co-X vs X)
Arthur-Merlin protocols, zero-knowledge proofs, probabilistically checkable proofs, interactive proof systems to (i) allow applicant to preserve privacy of some information, (ii) allow certification authority to sample some evidence, (iii) allow certification authority to detect if an applicant is cheating. Of particular interest is the case where the applicant is not just claiming to have performed a computation but is also taking measurement of the “real-world” and the certification authority is interested in checking if the applicant has really taken these measurements.
Program checking to allow checking the output of complex calculation (or proof)
Application of the aforementioned ideas in less formal settings (e.g., assurance case)
Use of explanation in a challenge-response protocol between applicant and certification authority
Use of explanation as interface between human designers in different teams
Inspecting part of an explanation while maintaining some confidence in the claim that it explains
Verification procedure that creates a perturbed question from the original question and answers both questions and the perturbed question differs from the original question as little and their answers differ as much as possible
Design principles that facilitate explainability (are some schedulers, e.g. TT, easier to explain? are systems that are more “deterministic” easier to explain?)
Explainability in other domains (e.g., AI) and their use in explainability of real-time systems
Re-interpretation of previously known results (e.g., schedulability tests) in view of explainability
Explainability of tools that rely on measurements (e.g., measurement-based WCET analysis)
Explainability of real-time systems results in safety engineering
Assurances case as a form of explainability
Explanations on how design elements satisfy requirements (tracing)
Explanation of why a property of the physical world (e.g., the state of a plant controlled by a controller) is satisfied/violated because of an event in the cyber-realm (e.g., deadline miss of control software)
Explanations that encourage human engagement and curiosity (i.e., don't dump a large volume of explanations/arguments that kill human curiosity)
If a problem comes in two variants, an optimization problem and a decision problem, can the optimization problem variant provide an explanation to the decision problem variant?
Root cause analysis
Contrastive explanation