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

[Bruce Lewis]

Dear All,

We had 25 on-line for Dr. John Hatcliff's HAMR presentation/abstract 
below.  Lots of questions.  We recorded the session and chat 
transcript.  If you get a chance to review it before the January AADL 
Technology Update, it provides the context for the next presentation in 
January on GUMBO, a contract language that works with AADL and HAMR to 
specify behavior contracts both on the architecture and then down to the 
components for formal verification, including within the the component.

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:

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

GUMBO is an exploratory AADL contract language effort still under 
development.  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 with 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 
toolset provides an understandable correspondence between models and 
verifiable implementations. Using the toolset, 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:

meet.google.com/not-tvtf-jbu


Dr. Jerome Hugues will be leading the AADL Standard session to plan 
priority topics for review and update on January 19th. Discuss list of 
topics and gather feedback on priorities, including:

AADL core: semantics of modes;

  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. 
https://github.com/saeaadl/emv2

Join with Google Meet at 11 AM ET, 10AM

meet.google.com/ihj-nvca-nxd

Thanks,

Bruce Lewis,

AADL Committee Chair







On 11/23/2022 11:56 AM, Bruce Lewis wrote:
>
> 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
>
>
>
>
>
-- 
Bruce Lewis
256-468-4902
256-919-6627

-------------- next part --------------
HTML attachment scrubbed and removed
-------------- next part --------------
HTML attachment scrubbed and removed
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 840 bytes
Desc: OpenPGP digital signature
URL: <http://lists.sei.cmu.edu/pipermail/sae-aadl-users/attachments/20221223/fd857240/attachment-0001.sig>