[aadl]: AADL Virtual Meetings in January 2022, with email corrections. Jan 18 ->10-11AM CT. Jan 19 ->10:00-11:30 AM CT

[Bruce Lewis]

Dear All,

Sorry for the unfinished email that preceded this one.  Here's the update.

We had 25 participants for our November Google Meet with Dr. John 
Hatcliff's HAMR presentation (abstract below).  We recorded the session 
and the chat transcript.  If you get a chance to review it before the 
January AADL Technology Update, it provides context for the next 
presentation in January on GUMBO.

Web address for the HAMR video: 
https://drive.google.com/file/d/1ahgYWh5iu5SvHUISOu_7EH1jNwospC4S/view

Web address for the chat transcript: 
https://drive.google.com/file/d/1xa1rzEflvfA0sO2QesFT3SQBRosEvOtN/view


January AADL meetings:

On January 18th, Dr. Danielle Stewart, of Galois, will be presenting GUMBO.

GUMBO is an AADL contract language currently under research & 
development at Galois along with John Hatcliff at KSU.  GUMBO reduces 
the gap between model-level behavior specifications and the verification 
of the behavior of deployed code. We developed a model-level behavior 
specification language and provided full development support. We 
designed this first order logic specification language in tandem with a 
formalization of AADL model-level semantics. We then developed the 
capability to automatically translate these specifications from the 
model down to the generated code via the High Assurance Modeling and 
Rapid engineering framework (HAMR). HAMR also auto-generates the 
partitioning and information flow policies for the seL4 micro-kernel, 
based on the topology of the components and connections in the 
architecture model. The software implementation, with its corresponding 
contracts, may then be verified using our Logika formal verification 
tool, which handles reasoning about the contracts generated from the 
specification language. The resulting integrated tool set provides an 
understandable correspondence between models and verifiable 
implementations. Using the tool set, developers can specify both 
architecture and behavior of the system at the model level, 
auto-generate code that can be deployed on the system, and then formally 
verify that the code behavior satisfies the requirements specified at 
the model level.

Join with Google meet on Jan18 from 10:00-11:00 Central Time,web 
address:  meet.google.com/not-tvtf-jbu

On January 19th,  Dr. Jerome Hugues will be leading the AADL Standard 
session.  We will discuss a list of topics and gather feedback on 
priorities, including:  1) AADL core: semantics of modes; 2) EMV2: 
review issues, many are critical issues in the semantics of the language 
itself and how to interpret some constructs.  This is especially 
critical as those rules specify how to compute probabilities.   See the 
errata at: https://github.com/saeaadl/emv2

Join with Google Meet on Jan 19 at 10:00-11:30 AM Eastern Time, web 
address:  meet.google.com/ihj-nvca-nxd

Thanks, Bruce Lewis, AADL Committee Chair


Prior AADL Technology session on HAMR ========================================================

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.

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


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