Digital Library
In this podcast, James Edmondson and Sagar Chaki describe an architecture and approach to engineering high-assurance software for Distributed Adaptive Real-Time (DART) systems.
Watch Sagar Chaki in this SEI Cyber Minute as he discusses "Assuring Autonomous Software".
Topics: Software Assurance
This paper presents two challenge problems guiding research on developing a provably correct approach for runtime assurance of distributed real-time embedded systems.
Topics: Cyber-Physical Systems
Cyber-physical systems (CPS) integrate computational algorithms and physical components. SEI promotes efficient development of high-confidence, distributed CPS.
Topics: Process Improvement
Predictability by construction (PBC) makes the behavior of a component-based system predictable before implementation, based on known properties of components.
This work is producing validated assurance techniques for distributed adaptive real-time (DART) systems
Software that accesses the system clock is the key to real-time and cyber-physical systems
Formally verify STACs at the source code level using deductive (aka auto-active) verification
DART Vision
In this paper, the authors focus on proving the correctness of the budget enforcement that guarantees that no task τi executes beyond its W1 i. They present their approach and some preliminary results.
Topics: Cyber-Physical Systems
This paper provides an end-to-end framework where DART systems can be designed, analyzed, and implemented within the same toolchain. In this talk, the authors present this toolchain and demonstrate it on a few representative examples.
This work proposes a bridge between two important verification methods, software model checking and hybrid systems reachability.
In this conference paper, the authors describe an approach to Statistical Model Checking (SMC). This paper is part of the Lecture Notes in Computer Science book series.
Topics: Cyber-Physical Systems
DMPL is a language for programming distributed real-time, mixed-criticality software. It supports distributed systems in which each node executes a set of periodic real-time threads that are scheduled by priority and criticality.
This paper presents three variants of multi-threaded IC3s for model checking hardware, differing by degree of synchronization and aggressiveness of proof checking.
This presentation describes an evidence-based approach for producing high-assurance DART software involving multiple layers of the CPS stack.
This poster describes the authors' research efforts in verifying distributed adaptive real-time systems.
This 2015 Research Review presentation describes the authors' research efforts in verifying distributed adaptive real-time systems.
In this 2015 Research Review presentation, the author describes his research efforts into scaling up software model checking—a fundamental challenge in the field.
This short paper introduces our architecture and approach to engineering a DART system so that we achieve high assurance in its runtime behavior against a set of formally specified requirements.
Topics: Malware Analysis
In this article, the authors present a notion of similarity based on provenance; two binaries are similar if they are compiled from the same source code with the same compilers.
Topics: Malware Analysis
In this article, the authors present an alternative to pair wise comparisons based on "hashing” that captures the semantics of functions as semantic hashes.
Topics: Malware Analysis
In this article, the authors present a static approach that uses symbolic execution and inter-procedural data flow analysis to discover object instances, data members, and methods of a common class.
Topics: Cyber-Physical Systems
In this paper, the authors advocate, formalize, and empirically justify an approach to compute quantitative utility of robotic missions using probabilistic model checking.
This report describes line-funded exploratory new starts (LENS) projects that were conducted during fiscal year 2012 (October 2011 through September 2012).
This article introduces a reliability engineering assurance approach based on probabilistic model checking.
This report describes the line-funded exploratory new starts (LENS) projects that were undertaken during fiscal year 2011. For each project, the report presents a brief description and a recounting of the research that was done, as well as a synopsis of the results of the project.
Topics: Acquisition Support
In this report, the authors describe work to develop standards for automated remediation of vulnerabilities and compliance issues on DoD networked systems.
Topics: Cyber-Physical Systems
This presentation considers the problem of verifying functional correctness of periodic Real-Time Embedded Software (RTES), a popular variant of RTES that execute periodic tasks in an order determined by Rate Monotonic Scheduling (RMS).
Topics: Acquisition Support
In this report, the authors describe work to develop standards for vulnerability and compliance remediation on DoD networked systems.
Topics: Software Architecture
In this report, the authors present COVERT, an automated framework for finding buffer overflows in C programs using software verification tools and techniques.
Sagar Chaki and others describe in this presentation an implementation of the approach that targets the Pin component technology, and presents experimental results on a collection of benchmarks.
Topics: Software Assurance
In this report, the authors present an approach to certify binary code against expressive policies to achieve the benefits of PCC and CMC.
This report describes the IRAD projects that were conducted during fiscal year 2006 (October 2005 through September 2006).
Copper is a software model checker for concurrent message-passing C programs.
Paper from the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2007.
This report shows how L^F can be used for compositional regular failure language containment and deadlock detection, using non-circular and circular assume-guarantee rules.
Topics: Software Assurance
In this report, the authors present a technique for certifying the safety of buffer manipulations in C programs.
This 2006 report presents a technique that uses proofs to certify software.
In this paper, the authors present an automated overflow detection technique based on model checking and iterative refinement.
Topics: Software Architecture
This 2005 report describes the application of the SEI Architecture Tradeoff Analysis Method (ATAM) to the U.S. Army's Warfighter Information Network-Tactical (WIN-T) system.
This report describes the IR&D projects that were conducted during fiscal year 2005 (October 2004 through September 2005). In addition, this report provides information on what the SEI has learned in its role as a technology scout for developments over the past year in the field of software engineering.
Model checking is a promising technology for verifying critical behavior of software. However, software model checking is hamstrung by scalability issues and is difficult for software engineers to use directly. ComFoRT addresses both of these challenges.
Predicate abstraction is a popular abstraction technique employed in formal software verification. Experiments show that predicate minimization can result in a significant reduction of both verification time and memory usage compared to earlier methods.