Embedded systems are controlling an increasing amount of the automotive experience, from infotainment systems and connectivity to drivers’ portable devices to driver assist and vehicle safety/control features, making them smarter, but also more complex. Often contrary to the safety-critical nature of some embedded automotive systems are short development cycles; there isn’t always time to make sure these systems are 100 percent bug free before they’re deployed in vehicles. Arizona State University’s Center for Embedded Systems (CES) is working on developing a software tool that can improve confidence in these designs.

An area of CES’s research is based on the method of Model Based Development (MBD). In MBD, the system design and development always starts with a mathematical model of the system, with which system designers use to verify that the model satisfies the system’s specifications. MBD has several advantages over traditional system development methods; particularly, by utilizing MBD practices, the main design choices are evaluated on the model of the system, removing the need for building costly prototypes.

Georgios Fainekos, Assistant Professor, School of Computing, Informatics and Decision Systems Engineering at Arizona State University, is focused on MBD tools for Cyber Physical Systems (CPSs), or embedded systems that actively interact with the physical components of a control system – such as a car engine model or a person’s body in the case of medical devices – and computations and communications that control the physical components. In automotive systems, CPSs include systems like drive by wire, ABS, and engine control. CES’s focus on CPSs is achieving safety-critical dependability.

Fainekos, along with Dr. Sriram Sankaranarayanan at the University of Colorado, Boulder, has been developing the S-TALIRO or Systems TemporAL LogIc RObustness set of tools (Figure 1) over the last 5 years. It performs simulations to check the system model for behaviors that do not comply with system specifications, such as that the engine doesn’t stall while the vehicle is cruising. In addition to checking for failures to meet specifications as many verification strategies do, it also checks for behaviors that produce close to the failure the simulation is looking for. In other words, it can find behaviors that will potentially fail the specifications and isn’t restricted to finding actual failures, which means catching more potential, and potentially dangerous, bugs, thus giving system designers more confidence in their designs.

One potential effect of using S-TALIRO to analyze CPSs is to prevent recalls due to software errors that may slip through other methods of design verification. According to the CES, the complexity of modern automotive systems is influencing the industry to move into MBD practices to address the need for tools that can verify the correctness of a system’s functional requirements. According to industry reports, software testing accounts for up to 22 percent of the total cost of a new vehicle. With the use of a tool like S-TALIRO, testing costs can be reduced by anywhere from 5 percent to 35 percent. CES member companies are experimenting with S-TALIRO in their applications, and the tools were nominated in 2012 as a Technology Breakthrough of NSF Industry/University Cooperative Research Centers (I/UCRC).

This year, Fainekos and his research team are focusing on creating a Graphical User Interface (GUI) for the tool. S-TALIRO relies on formal logic to formalize system requirements. The logic specifies when the system can perform what operations and not get unintended actions that could cause failures or potential failures. Writing the logic for these types of systems is not what engineers typically do and can require formal logic training. To make this system useful for those without formal training in logic, they are building a user interface that allows engineers to use the tools without having to write the underlying logic. Ideally, in the very long term, they want to come up with a system that can take the desired requirements, a partial model of the system, and synthesize the software so it satisfies the requirements. However, Fainekos says, “Once you can get it to that level it’s the Holy Grail. The software design will come with formal correctness guarantees, and the time spent for testing and verification will be reduced substantially.”

For more information, visit the TALIRO tools website:

http://opsy.st/ECDFeb14TALIRO