Over-the-air (OTA) updates are becoming a standard practice for upgrading Cyber-Physical Systems (CPS) software, allowing software systems to be modified through a wireless network. They are beneficial in several contexts. For example, in the automotive domain, OTA updates enable manufacturers to update vehicle software without physical access. However, the considerable number of products (e.g., vehicles within the fleet) and frequent changes and updates to software components can generate many software configurations that are impossible to analyze beforehand without any automated support. This problem hampers the verification of the system’s safety. This paper proposes a contract-driven framework for reasoning about the safety of OTA updates. Our framework supports (a)contract composition, which enables reasoning about the behavior composition of different software components, and (b) verification ofcomponent substitutability, which allows checking if the software component deployed by an OTA update can replace another component without generating any safety breach.We rigorously define our framework and formally prove that if the OTA update ensures the satisfaction of its contract, the system (safety) properties are preserved. We propose an instance of our solution that targets CPS designed with Simulink®System Composer, a widely used tool for modeling the different components of the system architecture and their interaction. We propose using Simulink®Requirements Tables to express the contracts of CPS components, as they enable engineers to model the system requirements using pre/post-conditions within their Simulink®models. We implemented our solution as a software prototype that extends THEANO, a tool that enables engineers to verify the consistency and completeness of Requirements Tables. We evaluated our solution by considering the Ten Lockheed Martin Cyber-Physical Problems. We defined 20 OTA updates and effectively identified issues in 9 of them. We analyzed and fixed the problems, inspecting each unsafe OTA update to understand the causes of the safety breaches. After fixing the problems, THEANO confirmed the safety of all OTA updates. THEANO required less than a minute to analyze each OTA update, making it practical for industrial applications.

Operational Design Domain (ODD) attributes define the environmental conditions under which Automated Driving Systems (ADS) can safely operate. These attributes include factors such as road and lighting conditions, as well as infrastructure elements, such as lane markings and road conditions. However, existing ODD definitions are often ambiguous and lack specificity, making it challenging to validate their presence in datasets.The absence of precise ODD definitions and robust validation mechanisms poses significant challenges, as it remains unclear whether ADS training and testing datasets adequately represent real-world operating conditions. This gap introduces risks that could compromise the safe deployment of ADS in diverse environments.To address this issue, we introduce FODSE (Framing ODDs as Domain Specifications for Evaluation), a semi-automated AI-powered approach that refines ODD attributes into structured, context-aware domain specifications and systematically evaluates their presence in datasets. FODSE leverages Retrieval-Augmented Generation (RAG), multimodal AI, and prompt learning to enhance specification clarity and dataset completeness.Experimental evaluation on two commonly adopted datasets in ADS demonstrates that FODSE significantly improves dataset validation accuracy, achieving up to 96.8% classification accuracy for an extended set of lane marking variants and 97.8% for roadway users—two key ODD attributes. Expert assessments confirm that FODSE effectively reduces ambiguity and enhances contextual adaptability, reinforcing its potential to improve dataset integrity and ensure safer, more reliable ADS training and validation.

Deep Neural Networks (DNNs) are increasingly deployed across a wide range of applications, from image classification to autonomous driving. However, ensuring their reliability remains a challenge, and in many situations, alternative models with similar functionality and accuracy levels are available. Traditional accuracy-based evaluations often fail to capture behavioral differences between such models, particularly when testing datasets are limited, making it challenging to select or optimally combine models. Differential testing addresses this limitation by generating test inputs that expose discrepancies in the behavior of DNN models. However, existing differential testing approaches face significant limitations: many rely on access to model internals or are constrained by the availability of seed inputs, limiting their generalizability and effectiveness. In response to these challenges, we proposeDiffGAN, a black-box test generation approach for differential testing of DNN models. Our approach, though adaptable to other domains, is specific to DNN models for image classification tasks, a highly prevalent application area. Our method relies on a Generative Adversarial Network (GAN) and the Non-dominated Sorting Genetic Algorithm II (NSGA-II) to generate diverse and valid triggering inputs that effectively reveal behavioral discrepancies between models. Our method employs two custom fitness functions, one focused on diversity and the other on divergence, to guide the exploration of the GAN input space and identify discrepancies between the models’ outputs. By strategically searching the GAN input space, we show thatDiffGANcan effectively generate inputs with specific features that trigger differences in behavior for the models under test. Unlike traditional white-box methods,DiffGANdoes not require access to the internal structure of the models, which makes it applicable to a wider range of situations. We evaluateDiffGANon a benchmark comprising eight pairs of DNN models trained on two widely used image classification datasets. Our results demonstrate thatDiffGANsignificantly outperforms a state-of-the-art (SOTA) baseline, generating four times more triggering inputs, with higher diversity and validity, within the same testing budget. Furthermore, we show that the generated input can be used to improve the accuracy of a machine learning-based model selection mechanism, which dynamically selects the best-performing model based on input characteristics and can thus be used as a smart model output voting mechanism when using alternative models together.

Deep Reinforcement Learning (DRL) has made significant advancements in various fields, such as autonomous driving, healthcare, and robotics, by enabling agents to learn optimal policies through interactions with their environments. However, the application of DRL in safety-critical domains presents challenges, particularly concerning the safety of the learned policies. DRL agents, which are focused on maximizing rewards, may select unsafe actions, leading to safety violations. Runtime safety monitoring is thus essential to ensure the safe operation of these agents, especially in unpredictable and dynamic environments. This paper introducesSMARLA, a black-box safety monitoring approach specifically designed for DRL agents.SMARLAutilizes machine learning to predict safety violations by observing the agent's behavior during execution. The approach is based on Q-values, which reflect the expected reward for taking actions in specific states.SMARLAemploys state abstraction to reduce the complexity of the state space, enhancing the predictive capabilities of the monitoring model. Such abstraction enables the early detection of unsafe states, allowing for the implementation of corrective and preventive measures before incidents occur. We quantitatively and qualitatively validatedSMARLAon three well-known case studies widely used in DRL research. Empirical results reveal thatSMARLAis accurate at predicting safety violations, with a low false positive rate, and can predict violations at an early stage, approximately halfway through the execution of the agent, before violations occur. We also discuss different decision criteria, based on confidence intervals of the predicted violation probabilities, to trigger safety mechanisms aiming at a trade-off between early detection and low false positive rates.

Over the past two decades, the volume of electronics and software in cars have grown tremendously. But this growth has also resulted in hardware and software architectures that are proving to be a bottleneck for further innovation and efficient design flows, especially when implementing compute-intensive functions necessary for modern autonomous features. For example, centralized architectures that are driven by the use of more powerful processors result in higher sensor-to-actuator delays. Similarly, timing uncertainties increase as signal-based in-vehicle communication is being replaced by more dynamic service-oriented communication architectures. Finally, the increasing volume of software running on powerful multicore ECUs is making timing analysis, including WCET estimation, to be very complex. As a result, timing estimates, when safe, are very pessimistic, which makes efficient implementations to be difficult. In this position paper, we outline some of these emerging challenges and discuss potential solutions.

Deep Neural Networks (DNNs) have been extensively used in many areas including image processing, medical diagnostics and autonomous driving. However, DNNs can exhibit erroneous behaviours that may lead to critical errors, especially when used in safety-critical systems. Inspired by testing techniques for traditional software systems, researchers have proposed neuron coverage criteria, as an analogy to source code coverage, to guide the testing of DNNs. Despite very active research on DNN coverage, several recent studies have questioned the usefulness of such criteria in guiding DNN testing. Further, from a practical standpoint, these criteria are white-box as they require access to the internals or training data of DNNs, which is often not feasible or convenient. Measuring such coverage requires executing DNNs with candidate inputs to guide testing, which is not an option in many practical contexts. In this paper, we investigate diversity metrics as an alternative to white-box coverage criteria. For the previously mentioned reasons, we require such metrics to be black-box and not rely on the execution and outputs of DNNs under test. To this end, we first select and adapt three diversity metrics and study, in a controlled manner, their capacity to measure actual diversity in input sets. We then analyze their statistical association with fault detection using four datasets and five DNNs. We further compare diversity with state-of-the-art white-box coverage criteria. As a mechanism to enable such analysis, we also propose a novel way to estimate fault detection in DNNs. Our experiments show that relying on the diversity of image features embedded in test input sets is a more reliable indicator than coverage criteria to effectively guide DNN testing. Indeed, we found that one of our selected black-box diversity metrics far outperforms existing coverage criteria in terms of fault-revealing capability and computational time. Results also confirm the suspicions that state-of-the-art coverage criteria are not adequate to guide the construction of test input sets to detect as many faults as possible using natural inputs.

Deep Reinforcement Learning (DRL) algorithms have been increasingly employed during the last decade to solve various decision-making problems such as autonomous driving, trading decisions, and robotics. However, these algorithms have faced great challenges when deployed in safety-critical environments since they often exhibit erroneous behaviors that can lead to potentially critical errors. One of the ways to assess the safety of DRL agents is to test them to detect possible faults leading to critical failures during their execution. This raises the question of how we can efficiently test DRL policies to ensure their correctness and adherence to safety requirements. Most existing works on testing DRL agents use adversarial attacks that perturb states or actions of the agent. However, such attacks often lead to unrealistic states of the environment. Furthermore, their main goal is to test the robustness of DRL agents rather than testing the compliance of the agents' policies with respect to requirements. Due to the huge state space of DRL environments, the high cost of test execution, and the black-box nature of DRL algorithms, exhaustive testing of DRL agents is impossible. In this paper, we propose a Search-based Testing Approach of Reinforcement Learning Agents (STARLA) to test the policy of a DRL agent by effectively searching for failing executions of the agent within a limited testing budget. We rely on machine learning models and a dedicated genetic algorithm to narrow the search toward faulty episodes (i.e., sequences of states and actions produced by the DRL agent). We apply STARLA on Deep-Q-Learning agents trained on two different RL problems widely used as benchmarks and show that STARLA significantly outperforms Random Testing by detecting more faults related to the agent's policy. We also investigate how to extract rules that characterize faulty episodes of the DRL agent using our search results. Such rules can be used to understand the conditions under which the agent fails and thus assess the risks of deploying it.

Abstract With the increasing demand for customized systems and rapidly evolving technology, software engineering faces many challenges. A particular challenge is the development and maintenance of systems that are highly variable both in space (concurrent variations of the system at one point in time) and time (sequential variations of the system, due to its evolution). Recent research aims to address this challenge by managing variability in space and time simultaneously. However, this research originates from two different areas, software product line engineering and software configuration management, resulting in non-uniform terminologies and a varying understanding of concepts. These problems hamper the communication and understanding of involved concepts, as well as the development of techniques that unify variability in space and time. To tackle these problems, we performed an iterative, expert-driven analysis of existing tools from both research areas to derive a conceptual model that integrates and unifies concepts of both dimensions of variability. In this article, we first explain the construction process and present the resulting conceptual model. We validate the model and discuss its coverage and granularity with respect to established concepts of variability in space and time. Furthermore, we perform a formal concept analysis to discuss the commonalities and differences among the tools we considered. Finally, we show illustrative applications to explain how the conceptual model can be used in practice to derive conforming tools. The conceptual model unifies concepts and relations used in software product line engineering and software configuration management, provides a unified terminology and common ground for researchers and developers for comparing their works, clarifies communication, and prevents redundant developments.

Software Product Lines (SPLs) are families of related software products developed from a common set of artifacts. Most existing analysis tools can be applied to a single product at a time, but not to an entire SPL. Some tools have been redesigned/re-implemented to support the kind of variability exhibited in SPLs, but this usually takes a lot of effort, and is error-prone. Declarative analyses written in languages like Datalog have been collectively lifted to SPLs in prior work [1], which makes the process of applying an existing declarative analysis to a product line more straightforward. In this paper, we take an existing declarative analysis (behaviour alteration) and apply it to a set of automotive software product lines from General Motors. We discuss the design of the analysis pipeline used in this process, present its scalability results, and provide a means to visualize the analysis results for a subset of products filtered by feature expression. We also reflect on some of the lessons learned throughout this project.

The emerging Die-stacking technology enables DRAM to be used as a cache to break the “Memory Wall” problem. Recent studies have proposed to use DRAM as a victim cache in both CPU and GPU memory hierarchies to improve performance. DRAM caches are large in size and, hence, when realized as a victim cache, non-inclusive design is preferred. This non-inclusive design adds significant differences to the conventional DRAM cache design in terms of its probe, fill, and writeback policies. Design and verification of a victim DRAM cache can be much more complex than that of a conventional DRAM cache. Hence, without rigorous modeling and formal verification, ensuring the correctness of such a system can be difficult. The major focus of this work is to show how formal modeling is applied to design and verify a victim DRAM cache. In this approach, we identify the agents in the victim DRAM cache design and model them in terms of interacting state machines. We derive a set of properties from the specifications of a victim cache and encode them using Linear Temporal Logic. The properties are then proven using symbolic and bounded model checking. Finally, we discuss how these properties are related to the dataflow paths in a victim DRAM cache.

The existing approaches to design efficient safety-critical control applications is constrained by limited in-vehicle sensing and computational capabilities. In the context of automated driving, we argue that there is a need to leverage resources “out-of-the-vehicle” to meet the sensing and powerful processing requirements of sophisticated algorithms (e.g., deep neural networks). To realize the need, a suitable computation offloading technique that meets the vehicle safety and stability requirements, even in the presence of unreliable communication network, has to be identified. In this work, we propose an adaptive offloading technique for control computations into the cloud. The proposed approach considers both current network conditions and control application requirements to determine the feasibility of leveraging remote computation and storage resources. As a case study, we describe a cloud-based path following controller application that leverages crowdsensed data for path planning.

Die-stacking technology enables the use of a high density DRAM as a cache. Major processor vendors have recently started using these stacked DRAM modules as the last level cache of their products. These stacked DRAM modules provide high bandwidth with relatively low latency compared to the off-package DRAM modules. Recent studies on DRAM caches propose several variants to optimize performance and power of the systems. However, none of the existing works discuss its design and verification aspect. DRAM cache controller (DCC) design is significantly complex in comparison to a conventional DRAM-based main memory controller. This is because it involves controlling both the timing aspect of DRAM system as well as the functional aspect of cache. Therefore, without rigorous modeling and verification of such designs, it would be difficult to ensure correctness. In the current research, we focus on the design and verification issues of DCC. We select a common variant of DRAM cache and build a formal model of its controller in terms of interacting state machines; we term the common variant as the baseline and its model as the base model. We then verify safety, liveness, and timing properties of this variant using model checking. Next, we demonstrate how the formal models and the associated properties of other variants of DCCs can be derived from the base model in a systematic way. Analyzing the individual DRAM cache variations, we observe that most of the variants exhibit product-line characteristics.

Modern automotive systems consist of hundreds of functionalities implemented in software. Moreover, these functionalities are constantly evolving with increasing demand for automation, industry competition and changing sensor and actuator capabilities. Correspondingly, it is important to adapt the engineering and software development processes for such systems to consider fast management of this evolution at minimum cost. Towards this, in this paper, we outline three different problems in the context of evolving automotive software and discuss potential solutions for each of them. First, we outline a framework that can accommodate variability in specifications while developing software for automotive product lines. Secondly, a technique is illustrated to addresses after-sales addition of new features in existing systems by studying corresponding acceptable performance degradation of existing functionalities. Finally, we discuss how an inconsistency management framework and regression verification can ensure consistent evolution of engineering processes for automotive mechatronic systems.

The fierce competition among automotive manufacturers in introducing Advanced Driver Assist Systems (ADAS) and autonomous features has led to the explosive growth of the Electrical/Electronics (E/E) assets, including Software, in today's and future vehicles. The resource demand and quality requirements of these assets has increased consequently. Rigorous methodologies and tools are required for developing the E/E assets to meet the quality demands of these assets. This paper summarizes the current practices used in the industry for managing the development of these assets and discusses the future trends. The summary includes the description of three development strategies that are becoming important and critical, which are Model-driven Feature Development, Product Line Approach and Virtual Development and Integration of E/E architectures.

Time-triggered architectures form an important component of many distributed computing platforms for safety-critical real-time applications such as avionics and automotive control systems. TTA, FlexRay, and TTCAN are examples of such time-triggered architectures that have been popular in recent times. These architectures involve a number of algorithms for synchronizing a set of distributed computing nodes for meaningful exchange of data among them. The algorithms include a startup algorithm whose job is to integrate one or more nodes into the group of communicating nodes. The startup algorithm runs on every node when the system is powered up, and again after a failure occurs. Some critical issues need to be considered in the design of the startup algorithms, for example, the algorithms should be robust under reasonable assumptions of failures of nodes and channels. The safety-critical nature of the applications where these algorithms are used demands rigorous verification of these algorithms, and there have been numerous attempts to use formal verification techniques for this purpose. This paper focuses on various formal verification efforts carried out for ensuring the correctness of the startup algorithms. In particular, the verification of different startup algorithms used in three time-triggered architectures, TTA, FlexRay, and TTCAN, is studied, compared, and contrasted. Besides presenting the various verification approaches for these algorithms, the gaps and possible improvements on the verification efforts are also indicated.

Modern automotive systems are composed of hundreds of software-implemented features often interacting with physical subsystems under real-time constraints. For efficient management of their development, the features are conceived and realized as product lines involving variability with different variants being deployed in different vehicle classes. The variability information is expressed at different levels of abstraction during the various phases of development, like requirements, design and implementation. We introduce and study a formal model of such feature product lines capable of capturing variability and real-time behavior. We define a notion of conformance to relate the variability at different levels of abstraction and propose a compositional method of verifying conformance of multiple features. The proposed approach naturally extends to hybrid system behaviors consisting of discrete and continuous plant variables. We demonstrate the applicability of the approach by giving a simple paradigmatic example.

Automotive software has been growing in size, criticality and complexity with each new generation of vehicles. Testing at the model and code level is an important step in validating the software against various types of defects that may be introduced in the development process. Model based testing (MBT) methodology, paves a road towards automation of testing activities. Test generation is a computationally complex task, which requires efficient constraint solving techniques and some guidance from the test engineer when this task cannot be solved by a tool. At the same time, automatic tools can hardly substitute domain testing experts which can develop more effective tests or at least test fragments than any tool. This is why we believe that future test generation tools should support "tester-in-the-loop" MBT approaches. In this paper, we provide a brief report on our results in this direction.

Automotive systems are turning out to be one of the most complex consumer electronic systems being ever built. For the modern day users, they are products like smartphones and tablets but in size, complexity and quality and safety requirements they match if not exceed aircraft, and similar high integrity systems. Many of the major advances in Software engineering like model based development, platform based design and product line engineering have been introduced in the development of automotive electronic and software subsystems, which involve million lines of code and tens of electronic control units interconnected with multiple communication buses. This talk will highlight the challenges, current practices and new developments in the industry in building next generation automotive software from the modeling and analysis perspective. The challenges include traditional issues like system integration and feature interaction arising out of the federated development model, heterogeneity in subsystem behavior, time and space distributed development of software and the recent and rapidly increasing demand for advanced driver assistance features and system level requirements like fault tolerance and security. The talk attempts to outline a set of requirements for modeling from the perspective of system design and analysis. The talk will also touch upon some of the research and developments efforts currently ongoing within and with our external partners to meet these challenges.

Today, most of the innovation in the automotive domain is in the areas of electronics and software. Modern cars have already been transformed, from largely mechanical entities, to complex embedded systems running on four wheels. High-end cars currently have around 100 electronic control units (ECUs), each with one or more, possibly multicore, processors. These ECUs communicate using different communication buses such as CAN, FlexRay, LIN, and more recently also Ethernet, and are connected to various cameras, radars, ultrasonic sensors, and also to a host of actuators. Such architectures are used to run several millions of lines of software code spanning across safety-critical, driver assistance, comfort, and entertainment related applications.

Code generators play a critical role in the Model Based Development of complex software systems. This is particularly true in the automotive domain, where the code auto-generated from Simulink/Stateflow models is directly flashed onto embedded controllers. Testing based approaches are popular for validating the translation of models to code. However, these approaches cannot guarantee the absence of bugs introduced during translation.

Abstract The design of a complex embedded control system involves integration of large number of components. These components need to interact in a timely fashion to achieve the system level end-to-end requirements. In practice, the component level timing specification consists of design attributes like component task mapping, task period and schedule definition but often lack details on their real-time (functional) requirements. As we observe, there is no systematic methodology in place for decomposing the feature level timing requirements into component level timing requirements. This paper proposes an early stagetime-budgeting methodologyto bridge the above gap. A salient proposal of this methodology is to considerparameterizedcomponent timing-requirements. A key step in the methodology involves computing a set of constraints by relating component requirements with feature requirements. This enables the separation of timing constraints from functionality decomposition, and facilitates early optimization of thecomponent time-budgetfor a complex component based embedded system. This paper formalizes the proposed methodology by using Parametric Temporal Logic. A case study involving two advanced features from the automotive domain, namely Adaptive Cruise Control and Collision Mitigation is given to demonstrate the methodology.

SUMMARY Model‐based test generation techniques based on random input generation and guided simulation do not satisfy the demands of high test coverage and completeness guarantees as required by safety‐critical applications. Recently, test generation techniques based on model checking have been reported to bridge this gap. To evaluate the effectiveness of these techniques, an in‐house tool suite, AutoMOTGen, has been developed for Simulink/Stateflow and applied on real‐life case studies at General Motors. This paper outlines the test generation methodology of AutoMOTGen and gives a comparative study with a commercial, primarily random input‐based, test generation tool on the same set of examples. The results indicate that in terms of coverage, model checking‐based techniques complement the random input‐based techniques. In addition, they provide proofs for unreachability that can aid in debugging the models. Therefore, it is recommended that model checking‐based tools be utilized to complement and enhance the effectiveness of model‐based testing methods in safety‐critical systems engineering. Copyright © 2013 John Wiley & Sons, Ltd.

Most innovations in the automotive domain are realized by electronics and software. Modern cars have up to 100 Electronic Control Units (ECUs) that implement a variety of control applications in a distributed fashion. The tasks are mapped onto different ECUs, communicating via a heterogeneous network, comprising communication buses like CAN, FlexRay, and Ethernet. For electric vehicles, software functions play an essential role, replacing hydraulic and mechanic control systems. While model-based software development and verification are already used extensively in the automotive domain, their importance significantly increases in electric vehicles as safety-critical functions might no longer rely on mechanical (fall-back) solutions. The need for reducing costs, size, and weight in electric vehicles has also resulted in a considerable interest in topics such as the consolidation of ECUs as well as efficient implementation of control software. In this paper we discuss two broad issues related to model-based software development and verification in electric vehicles. The first is concerned with how to ensure that model-level semantics are preserved in an implementation, which has important implications on the verification and certification of control software. The second issue is related to techniques for reducing the computational and communication demands of distributed automotive control algorithms. For both these topics we provide a broad introduction to the problem followed by a discussion on state-of-the-art techniques.

The Simulink/Stateflow (SL/SF) modeling framework is widely used in industry for the development of control applications. However, such models are not amenable to formal reasoning. Controllers can also be designed using formal specification languages. Such designs can be formally verified, but the models do not explicitly represent control or data flow information. In this paper, we discuss RRM diagrams (RRMDs), a new modelling notation which incorporates the benefits of these two formalisms. RRMDs are graphical formal models and they also support incremental formal development. We have used synchronising state machines to encode RRMDs. We have also developed a prototype tool which translates RRMDs automatically to SL/SF designs.

Simulink/Stateflow (SL/SF) is the primary modeling notation for the development of control systems in automotive and aerospace industries. In model based testing, test cases derived from a design model are used to show model-code conformance. Safety standards such as ISO 26262 recommend model based testing to show the conformance of a software with the corresponding model. From our experiments with various test generation techniques, we have observed that their coverage capabilities are complementary in nature. With this observation in mind, we have developed a new tool called SmartTestGen which integrates different test generation techniques. In this paper, we discuss SmartTestGen and the different test generation techniques utilized - random testing, constraint solving, model checking and heuristics. We experimented with 20 production-quality SL/SF models and compared the performance of our tool with that of two prominent commercial tools.

Correct functioning of automotive embedded controllers requires hard real-time constraints on a number of system parameters. To avoid costly design iterations, these timing constraints should be verified during the design stage itself. In this paper, we describe a formal verification technique for a class of timing constraints called timing synchronization constraints in the recent adaptation of AUTOSAR standard (WPII-1.2 Timing Subgroup, Release 4.0). These constraints require, unlike the well studied end-to-end latency constraint, simultaneous analysis of multiple task/message chains or multiple data items traversing through a task/message chain. We show that they can be analyzed by model-checking with finite-state monitors. We also demonstrate this method on a case-study from the automotive domain.

The modern automobile is a complex electronic system with a number of features providing functionalities for driver and passenger convenience, control of the vehicle, and safety of the occupants. As new features are developed and introduced into the automobile, they interact with already existing features, sometimes resulting in undesirable behaviours. These undesirable interactions are often detected very late in the development cycle, or sometimes even in the field. This introduces uncertainty in the system development process as changes to address these interactions often result in a cascading series of changes whose scope is difficult to predict. This paper presents a method and algorithms for identifying and resolving feature interactions early in the development life-cycle by addressing the problem at the level of requirements specifications. We have applied this method successfully in the automotive domain and present a case study of detecting and resolving feature interactions.

In a Software Product Line (SPL), the central notion of implementability provides the requisite connection between specifications (feature sets) and their implementations (component sets), leading to the definition of products. While it appears to be a simple extension (to sets) of the trace-ability relation between components and features, it actually involves several subtle issues which are overlooked in the definitions in existing literature. In this paper, we give a precise and formal definition of implementability over a fairly expressive traceability relation to solve these issues. The consequent definition of products in the given SPL naturally entails a set of useful analysis problems that are either refinements of known problems, or are completely novel. We also propose a new approach to solve these analysis problems by encoding them as Quantified Boolean Formula(QBF) and solving them through Quantified Satisfiability (QSAT) solvers. The methodology scales much better than the SAT-based solutions hinted in the literature and is demonstrated through a prototype tool called SPLANE (SPL Analysis Engine), on a couple of fairly large case studies.

SUMMARY This paper is concerned with test case generation from Simulink/Stateflow (SL/SF) models with a focus on coverage of SF model elements. Coverage of the SF component in a model is a difficult task because of two primary reasons: (i) the SF component itself may lie deep in the SL/SF model in which case, inputs have to pass through a complex chain of SL blocks to reach the SF block and (ii) nonlinear constraints in the model are difficult to solve using constraint solvers. Hierarchy and parallelism in the SF model add further complexity to the problem. The existing approaches flatten such SF elements, and generate test cases from the flattened finite state machines. Handling of issues (i) and (ii) has already been discussed in earlier research. In this paper, we present a method of covering SF components, which does not require to flatten any hierarchy or parallelism in the components. This not only makes the test case generation problem efficient but also addresses the problem of scalability. We have implemented this method and performed a number of medium‐sized case studies. The results show improved performance over the results obtained by some commercial tools. Copyright © 2011 John Wiley & Sons, Ltd.

The development of in-vehicle software, often controlling safety-critical functions related to braking, steering and transmission systems, requires rigorous techniques to ensure high-integrity and reliability requirements. Formal models of requirements and design artifacts based on state-transition systems and other formalisms serve as a means to apply rigorous analysis and verification techniques at every stage in the development process. We present here one such formal analysis and verification flow, developed at General Motors R&D, provide an overview of methods for automatic test generation based on mathematical modeling and discuss the future directions for research.

Exhaustive state space exploration based verification of embedded system designs remains a challenge despite three decades of active research into Model Checking. On the other hand, simulation based verification of even critical embedded system designs is often subject to financial budget considerations in practice. In this paper, we suggest an algorithm that minimizes the overall cost of producing an embedded system including the cost of testing the embedded system and expected losses from an incompletely tested design. We seek to quantify the trade-off between the budget for testing and the potential financial loss from an incorrect design. We demonstrate that our algorithm needs only a logarithmic number of test samples in the cost of the potential loss from an incorrect validation result. We also show that our approach remains sound when only upper bounds on the potential loss and lower bounds on the cost of simulation are available. We present experimental evidence to corroborate our theoretical results.

Automotive architectures today consist of up to 100 electronic control units (ECUs) that communicate via one or more FlexRay and CAN buses. Multiple control applications - like cruise control, brake control, etc. are specified as Simulink/Stateflow models, from which code is generated and mapped onto the different ECUs. In addition, scheduling policies and parameters, both for the ECUs and the buses, need to be specified. Code generation/optimization from the Simulink/Stateflow models, task partitioning and mapping decisions, as well as the parameters chosen for the schedulers all of these impact the execution times and timing behaviour of the control tasks and control messages. These in turn affect control performance, such as stability and steady-/transient-state behaviour. This paper discusses different aspects of this multi-layered design flow and the associated research challenges. The emphasis is on model-based code generation, analysis, testing and verification of control software for automotive architectures, as well as on architecture or platform configuration to ensure that the required control performance requirements are satisfied.

This paper presents a formal specification and analysis method motivated by issues faced during early stages of requirements development for automotive features. At this early stage of development, only overall goals of features are understood, and there is a need to discover all possible scenarios of operation. We have developed a formalism - Structured Transition Systems (STS) - that facilitates the rapid evolution of specifications. STS supports multiple idioms of specification : transitions, state-diagrams, scenarios etc. It also supports constructs for hierarchical organization of a specification. We have further defined analyses that are useful for review and inspection of STS specifications. A distinctive feature of our method is the ability to use analysis results to refine and reinforce parts of the specification by importing analysis results into STS specifications. In practice, this leads to a feedback loop where requirements can be rapidly refined using analysis engines to drive the development of requirements. We have experimented using our technique on a number of automotive case-studies, and we present some of our experiences with these case-studies.

The growing trend towards using component based design approach in embedded system development requires addressing newer system engineering challenges. These systems are usually time critical and require timing guarantees from components. The articulation of a desirable response bounds for the components is often ad-hoc and happens late in development. In this work, we present a formal methods based methodology for an early stage design space exploration. We focus on real-time response of a component as a basis for exploration and allow the developer model it using constant values or parameters. To quantify the parameters, we propose a novel constraint synthesis technique to correlate response times of interacting components. Finally, for system integration, we introduce a new notion of timing layout to specify time-budgeting for each component. The selection of a suitable layout can be made based on system optimization criteria. We have demonstrated our methodology on an automotive Adaptive Cruise Control feature.

This tutorial is concerned with various aspects of model-based design of hardware/software architectures of automotive systems. It will be split into three parts, the first dealing with model-based analysis of automotive ECU networks, the second with synthesis of schedules for such networks, and finally the third with model-based testing of such architectures.

Embedded control systems in automobiles are typically implemented by a set of tasks deployed on multiple Electronic Control Units (ECUs) communicating via one or more buses like CAN or FlexRay. In the case of safety-critical systems, there are hard real-time bounds on the (i) response times of tasks/messages, and (ii) end-to-end latencies of certain task/message chains. These depend on various factors like the number of tasks (and messages) involved in the processing (and communication) sequence, parameters of these tasks/messages, scheduling policies, communication protocols, clock drifts, etc. Moreover, since the data transfer among tasks/messages is typically via asynchronous buffers that are overwritable and sticky, multiple semantics are possible for end-to-end latency. Hence, precise estimation of response times and end-to-end latencies in embedded systems is a non-trivial problem.

We present the CoGenTe tool for automated black-box testing of code generators. A code generator is a program that takes a model in a high-level modeling language as input, and outputs a program that captures the behaviour of the model. Thus, a code generator's input and output are complex objects having not just syntactic structure but execution semantics, too. Hence, traditional test generation methods that take only syntax into account are not effective in testing code generators. CoGenTe amends this by incorporating various coverage criteria over semantics. This enables it to generate test-cases with a higher potential of revealing subtle semantic errors in code generators. CoGenTe has uncovered such issues in widely used real-life code generators: (i) lexical analyzer generators Flex and JFlex, and (ii) The MathWorks' simulator/code generator for Stateflow.

End-to-end latency of messages is an important design parameter that needs to be within specified bounds for the correct functioning of distributed real-time control systems. In this paper we give a formal definition of end-to-end latency, and use this as the basis for checking whether a stipulated deadline is violated within a bounded time. For unbounded verification, we model the system as a set of communicating Timed Automata, and perform reachability analysis. The proposed method takes into account the drift of clocks which is shown to affect the latency appreciably. The method has been tested on a medium sized automotive example.

Aimed at verifying safety properties and improving simula-tion coverage for hybrid systems models of embedded control software, we propose a technique that combines numerical simulation and symbolic methods for computing state-sets. We consider systems with linear dynamics described in the commercial modeling tool Simulink/Stateflow. Given an ini-tial state x, and a discrete-time simulation trajectory, our method computes a set of initial states that are guaranteed to be equivalent to x, where two initial states are consid-ered to be equivalent if the resulting simulation trajectories contain the same discrete components at each step of the simulation. We illustrate the benefits of our method on two case studies. One case study is a benchmark proposed in the literature for hybrid systems verification and another is a Simulink demo model from Mathworks.

The Simulink/Stateflow (SL/SF) environment from Math-works is becoming the de facto standard in industry for model based development of embedded control systems. Many commercial tools are available in the market for test case generation from SL/SF designs; however, we have observed that these tools do not achieve satisfactory coverage in cases when designs involve nonlinear blocks and Stateflow blocks occur deep inside the Simulink blocks.

This paper addresses the problem of testing auto-code generators. Auto-code generators take as input a model in certain modeling language, and produce as output a program that captures the execution semantics of the input-model. We focus on the problem of test specification for the purpose of automatically generating a test-suite. We propose a novel technique for test specification based on the execution behavior of models. We also propose an algorithm that uses such a behavioral test specification for directing test-case generation towards very specific behavioral patterns that we would like to exercise. We have implemented this technique, and have applied it for generating test-cases for a Stateflow auto-code generator.

It is now widely believed that FlexRay will emerge as the predominant protocol for in-vehicle automotive communication systems. As a result, there has been a lot of recent interest in timing and predictability analysis techniques that are specifically targeted towards FlexRay. In this paper we propose a compositional performance analysis framework for a network of electronic control units (ECUs) that communicate via a FlexRay bus. Given a specification of the tasks running on the different ECUs, the scheduling policy used at each ECU, and a specification of the FlexRay bus (e.g. slot sizes and message priorities), our framework can answer questions related to the maximum end-to-end delay experienced by any message, the amount of buffer required at each communication controller and the utilization of the different ECUs and the bus. In contrast to previous timing analysis techniques which analyze the FlexRay bus in isolation, our framework is fully compositional and allows the modeling of the schedulers at the ECUs and the FlexRay protocol in a seamless manner. As a result, it can be used to analyze large systems and does not involve any computationally expensive step like solving an ILP (which previous approaches require). We illustrate our framework using detailed examples and also present results from a Matlab-based implementation.

Model-based development is increasingly becoming the method of choice for developing embedded systems for applications in automotive and aerospace industries. It relies on tool-suites consisting of a variety of model-processing tools like simulators, model-translators and code-generators. The correctness of these tools used in the development process is a key requirement for safety critical applications. This paper proposes a novel testing methodology for the rigorous verification of model processing tools. The proposed methodology takes as input the syntactic and semantic meta-model of a modeling language, expressed in the form of inference rules. Using a coverage criteria over this meta-model, it generates test-models, and test-inputs for these test-models. Apart from testing the syntactic aspects of the translation, our method aims at testing subtle semantic interactions of the modeling language that are potentially mistranslated by the model-processing tools. We illustrate the methodology with a simple prototypical process calculus. We also report on the experiments carried out with Stateflow, a variant of hierarchical state-machines implemented in the Matlab/Simulink tool-suite

We address the problem of rigorous testing of program generators. Program generators are software that take as input a model in a certain modeling language, and produce as output a program that captures the execution semantics of the input-model. In this sense, program generators are also programs and, at first sight, the traditional techniques for testing programs ought to be applicable to program generators as well. However, the rich semantic structure of the inputs and outputs of program generators poses unique challenges that have so far not been addressed sufficiently in the testing literature. We present a novel automatic test-case generation method for testing program generators. It is based on both syntax and semantics of the modeling language, and can uncover subtle semantic errors in the program generator. We demonstrate our method on flex, a prototypical lexical analyzer generator.

Automated synthesis of monitors from high-level properties plays a significant role in assertion-based verification. We present a methodology to synthesize assertion monitors from visual specifications given in CESC (Clocked Event Sequence Chart). CESC is a visual language designed for specifying system level interactions involving single and multiple clock domains. It has well-defined graphical and textual syntax and formal semantics based on a synchronous language paradigm enabling formal analysis of specifications. We provide an overview of the CESC language with a few illustrative examples. The algorithm for automated synthesis of assertion monitors from CESC specifications is described. A few examples from standard bus protocols (OCP-IP and AMBA) are presented to demonstrate the application of the monitor synthesis algorithm.