Write a Blog >>
MODELS 2021
Sun 10 - Sat 16 October 2021
Sat 16 Oct 2021 00:40 - 01:00 at Room 2 - Certification and Assurance III Chair(s): Daniel Amyot

Cyber-physical systems, such as avionics, must be tolerant to cyber-attacks in the same way they are tolerant to random faults: they recover or safely shut down as requirements dictate. The DARPA Cyber Assured Systems Engineering program is developing design, analysis, and verification tools that enable systems engineers to design-in this cyber-resiliency in a Model-Based Systems Engineering environment. This paper discusses the automated model transformations that add in high-assurance components. These components are filters and monitors that prevent malicious input and detect supply chain attacks respectively. A formal specification defines each component and is used to verify that the component addresses system level cyber-requirements. Implementations are synthesized from the specification, and that synthesis is proven to preserve the exact meaning of the specification. The transformations are integrated into the Open Source AADL Tool Environment (OSATE). The paper further reports a case study applying these transformations to a UAV system that uses the Air Force Research Laboratory’s OpenUxAS services for route planning. Here the transforms add filters to guard against malformed input and monitors to guard against ground station spoofing and malicious flight plans from OpenUxAS.

Sat 16 Oct

Displayed time zone: Osaka, Sapporo, Tokyo change

00:00 - 01:00
Certification and Assurance IIITechnical Papers at Room 2
Chair(s): Daniel Amyot University of Ottawa
00:00
20m
Full-paper
Model-Based Development of Engine Control Systems: Experiences and Lessons LearntP&I
Technical Papers
Justin Cooper , Alfonso de la Vega University of York, Richard Paige McMaster University, Dimitris Kolovos University of York
00:20
20m
Full-paper
Exploring Architectural Design Decisions in Industry 4.0: A Literature Review and TaxonomyFT
Technical Papers
Tarik Terzimehic fortiss GmbH, Kirill Dorofeev fortiss GmbH, Sebastian Voss
00:40
20m
Full-paper
Synthesizing Verified Components for Cyber Assured Systems EngineeringP&I
Technical Papers