Search Results

Complex systems, such as modern advanced driver assistance systems (ADAS), consist of many interacting components. The number of options promises considerable flexibility for configuring systems with many cost-performance-value tradeoffs; however the potential unique configurations are exponentially many prohibiting a build-test-fix approach. Instead, engineering analysis tools for rapid design-space navigation and analysis can be applied to find feasible options and evaluate their potential for correct system behavior and performance subject to functional requirements. The OpenMETA toolchain is a component-based, design space creation and analysis tool for rapidly defining and analyzing systems with large variability and cross-domain requirements. The tool supports the creation of compositional, multi-domain components, based on a user-defined ontology, which captures the behavior and structure of components and the allowable interfaces.

In this paper, we consider smart charging and vehicle-to-home (V2H) technologies for plugin electric vehicles coordinated with home energy management systems (HEMS) for automated demand response. In this system, plugin electric vehicles automatically react to demand response events with or without HEMS’s coordination, while vehicles are charged and discharged (i.e., V2H) in appropriate time slots by taking into account demand response events, time-ofuse rate information, and users’ vehicle usage plan. We introduce three approaches on home energy management: centralized energy control, distributed energy control, and coordinated energy control. We implemented smart charging and V2H systems by employing two sets of standardized communication protocols: one using OpenADR 2.0b, SEP 2.0, and SAE standards and the other using OpenADR 2.0b, ECHONET Lite, and ISO/IEC 15118.

Autonomous vehicles (AVs) have already driven millions of miles on public roads, but even the simplest scenarios have not been certified for safety. Current methodologies for the verification of AV’s decision and control systems attempt to divorce the lower level, short-term trajectory planning and trajectory tracking functions from the behavioral rules-based framework that governs mid-term actions. Such analysis is typically predicated on the discretization of the state space and has several limitations. First, it requires that a conservative buffer be added around obstacles such that many feasible plans are classified as unsafe. Second, the discretized controllers modeled in this analysis require several refinement steps before being implementable on an actual AV, and typically do not allow the specification of comfort-related properties on the trajectories. Consumer-ready AVs use motion planning algorithms that generate smooth trajectories.

Optional software-based features (for example, to provide active safety, infotainment, etc.) are increasingly becoming a significant cost driver in automotive systems. In state-of-the-art production techniques, these optional features are built into the vehicle during assembly. This does not give the customer the flexibility to choose the specific set of features as per their requirement. They either have to buy a pre-bundled option that may or may not satisfy their preferences or are unable to find an exact combination of features from the inventory provided by a dealership. Alternatively, they have to pre-order a car from the manufacturer, which could result in a substantial delay. Therefore, it is important to improve the flexibility of delivering the optional features to customers. Towards this objective, the vehicle could be configured with the desired options at the dealership, when the customer requires them.

The Runtime Verification ECU (RV-ECU) is a new development platform for checking and enforcing the safety of automotive bus communications and software systems. RV-ECU uses runtime verification, a formal analysis subfield geared at validating and verifying systems as they run, to ensure that all manufacturer and third-party safety specifications are complied with during the operation of the vehicle. By compiling formal safety properties into code using a certifying compiler, the RV-ECU executes only provably correct code that checks for safety violations as the system runs. RV-ECU can also recover from violations of these properties, either by itself in simple cases or together with safe message-sending libraries implementable on third-party control units on the bus. RV-ECU can be updated with new specifications after a vehicle is released, enhancing the safety of vehicles that have already been sold and deployed.

Software verification is a critical component of software development. Software verification techniques include different forms of testing, inspection, static analysis, and formal verification. Formal verification offers the advantage that it corresponds, at least informally, to testing all possible paths through the software. There are two primary approaches to using formal verification to establish properties of software: (a) proving properties of a formal specification, and (b) proving an implementation is a refinement of its specification. The first approach allows inference of the proven properties of the implementation provided the implementation is correct. The second approach allows inference of the correctness of the implementation. Proving properties of a specification provides a means for detecting critical design flaws early in the development process. In model-based development, the model (e.g., a set of SIMULINK diagrams) is a formal specification of the desired system.