[aadl]: AADL/ACVIP Technology Update Session Dec 14, HAMR - High-Assurance Modeling and Rapid Engineering for Embedded Systems Using AADL

[Bruce Lewis]

Dear All,

Here's the abstract for the AADL Technology Update Session for 
December.  It will be Dec 14, starting 11am EST.  This would be 10AM 
Central, 5PM in Europe and 8AM PT.  Mark your calendar. Here's the link:

meet.google.com/xuo-uraq-dpu

========================================================

Title: HAMR - High-Assurance Modeling and Rapid Engineering for Embedded Systems Using AADL

Project Website:http://hamr.sireum.org

Presenter: John Hatcliff, Kansas State University

Collaborators: Adventium Labs (Galois, Inc) and Collins Aerospace

This talk will present an overview of HAMR (High-Assurance Modeling and Rapid Engineering) -- a multiple- platform code-generation, development, and verification tool-chain for AADL-specified systems. HAMR's architecture factors code-generation through AADL's standardized run-time services (RTS). HAMR uses the AADL RTS as an abstract platform-independent realization of execution semantics which can be instantiated by backend translations for different platforms. Current supported translation targets are: (1) Slang (a safety-critical subset of Scala with JVM-based deployment as well as C code generation designed for embedded systems), (2) Javascript (e.g., for rapid prototyping and illustration of system execution to stakeholders), (3) a C back-end for Linux with communication based on System V inter-process communication primitives, and (4) a C back-end for the seL4 verified micro-kernel being used in a number of US Department of Defense research projects. The C generated by HAMR is also compatible with the CompCert verified C compiler. HAMR supports integrations with other languages (e.g., CakeML) through its generated AADL RTS foreign-function interface facilities.

The talk will describe experience with HAMR on the DARPA CASE (Cyber-Assured System Engineering) project. On CASE, AADL is used to model defense systems and to enable component-based model-based transformations that enhance system architecture to achieve greater cyber-resiliency. HAMR is then used to support development and deployment on the seL4 microkernel. SeL4’s formally-verified partitioning and memory security properties provide the foundation for cyber-resiliency assurance arguments.

The talk will conclude with survey of current work on HAMR, including some teasers about the GUMBO AADL contract language and its translation to program-level Slang contracts with accompanying verification.  More details about GUMBO and Slang contracts will be presented in a future AADL committee talk.

Speaker Bio:

Dr. John Hatcliff is a University Distinguished Professor and Lucas-Rathbone Professor of Engineering at Kansas State University working in the areas of safety-critical systems, software architectures, and software verification and certification. He leads the Laboratory on Specification, Analysis, and Transformation of Software (SAnToS Lab), whose research has been funded by national funding agencies and companies including Department of Defense, National Science Foundation, DARPA, Department of Homeland Security, US Army, NASA, NIH, ARO, Air Force Office of Scientific Research, SEI, Collins Aerospace, Adventium Labs, and Lockheed Martin.


========================================================

Bruce





-------------- next part --------------
HTML attachment scrubbed and removed