Seminars

The increasing demand for automation in safety-critical applications such as aeronautics, automotive, industrial process control, medical devices and so on, has pressurized the need for scalable formal analysis techniques for ensuring reliable and error-free operation of the systems. A unique feature of these systems is the mixed discrete continuous behaviors they exhibit, which is due to the interaction between a digital computer controlling and a physical entity. From the point of view of computability, presence of the continuous dynamics makes the problem challenging so much so that the…

Proof-carrying code has been in existence since Necula and Lee coined the term in 1996. This talk brings forward the details of the development of proof-carrying code from control system specifications. The motivation for this work is the safety-critical nature of many control applications such as aeronautics, robot-assisted surgery, and ground transportation. Several challenges must be addressed during this effort, including: The formal representation of control-theoretic proofs; the migration and representation of these proofs across different layers of software implementation; and the…

Studies suggest that nearly all software errors are triggered by the interaction of no more than six parameters.  If so, testing all n-way combinations of parameters should provide high confidence that nearly all faults have been discovered.  This combinatorial testing is already used by dozens of companies.  Dr. Black will explain what combinatorial testing is and how to apply it to different situations.  Given 10 binary variables, can you exercise all triples with fewer than 20 tests?  He refers to free software available to generate such "covering arrays" for combinations of parameter…

Quality must be designed into and built into software.  Nevertheless testing (dynamic analysis) and static analyzers have roles in delivering excellent software.  Dr. Black will describe what static analysis is (and isn't) and compare it in general with testing.  Then he will talk about the dimensions of static analysis: universality, rigor, and subject matter, and concepts related to static analysis and their results.  Dr. Black will also share his views of the state of the art in static analyzers, citing results from the 2008, 2009, and 2010 Static Analysis Tool Expositions and other…

The artifacts of daily life are inexorably becoming more intelligent by means of embedded systems.  While this brings many advantages in terms of new functions, complexity is limiting progress.  Most UTRC activities in embedded and cyber-physical systems are focused on managing complexity in architectures and design processes in order to support emerging trends to increase functionality.  We will present some of these emerging trends and recent UTRC initiatives to address them, including the DARPA META II project involving MIT, UC Berkeley and UC Santa Barbara and the Autonomous and…