Authors: Darren Cofer, Isaac Amundson, Junaid Babar, David Hardin, Konrad Slind, Perry Alexander, John Hatcliff, Robby Array, Gerwin Klein, Corey Lewis, Eric Mercer, John Shackleton
IEEE Security & Privacy
Formal methods tools that provide mathematical proof of system properties have improved dramatically in their power and capabilities. Our team has developed a model-based systems engineering environment that integrates formal methods at all levels of…
Authors: Jason Belt, John Hatcliff, Robby Array, John Shackleton, Jim Carciofini, Todd Carpenter, Eric Mercer, Isaac Amundson, Junaid Babar, Darren Cofer, David Hardin, Karl Hoech, Konrad Slind, Ihor Kuz, Kent Mcleod
Journal of Systems Architecture
Verified microkernels such as seL4 provide trustworthy foundations for safety- and security-critical systems. However, their full potential remains unrealized due, in part, to the lack of application development environments that help engineers integrate…
SAE International Journal of Advances and Current Practices in Mobility-V132-99EJ
Certification standards for high-assurance systems include objectives for demonstrating compliance of process artifacts such as requirements and code with style guidelines and other standards. With the emergence of model-based development, similar…
Authors: Eric Mercer, Konrad Slind, Isaac Amundson, Darren Cofer, Junaid Babar, David Hardin
Software and Systems Modeling
Safety-critical systems such as avionics need to be engineered to be cyber resilient meaning that systems are able to detect and recover from attacks or safely shutdown. As there are few development tools for cyber resiliency, designers rely on guidelines…
Authors: Isaac Amundson, Darren Cofer, David Hardin, John Hatcliff
2024 AIAA DATC/IEEE 43rd Digital Avionics Systems Conference (DASC)
On the DARPA Cyber Assured Systems Engineering (CASE) program, our team has developed BriefCASE, an opensource model-based engineering environment for cyber-resilient system design. BriefCASE is comprised of tools that emit evidence of correctness, which…
Zero Trust Architecture requirements are of increasing importance in critical systems development. Zero trust tenets hold that no implicit trust be granted to assets based on their physical or network location. Zero Trust development focuses on…
Proceedings of the Workshop on Design Automation for CPS and IoT
Resolute is a tool and language for embedding an assurance argument in a system architecture model and evaluating the validity of the associated evidence. In this paper we report on a number of extensions to Resolute that support systems engineers in…
Authors: John Backes, Darren Cofer, Isaac Amundson
The Assume Guarantee Reasoning Environment (AGREE) is a compositional analysis tool for systems modeled in the Architecture Analysis and Design Language (AADL). It is compositional in that it can be used to prove properties about each layer of the…
Authors: Eric Mercer, Konrad Slind, Isaac Amundson, Darren Cofer, Junaid Babar, David Hardin
Model-Driven Engineering Languages and Systems (MODELS)
Cyber-physical systems, such as avionics, must be tolerant to cyber-attacks in the same way they are tolerant to random faults: they either gracefully recover or safely shut down as requirements dictate. The DARPA Cyber Assured Systems Engineering program…
Authors: Cong Liu, Junaid Babar, Isaac Amundson, Karl Hoech, Darren Cofer, Eric Mercer
NASA Formal Methods
Contract-based assume-guarantee reasoning can be used to improve the scalability of model checking by decomposing complex verification problems. In previous work, we demonstrated this approach for systems modeled using the Architecture Analysis and Design…
Feedback
Feedback
If you experience a bug or would like to see an addition on the current page, feel free to leave us a message.