Heating, ventilation, and air-conditioning (HVAC) system’s supervisory control is crucial for energy-efficient thermal comfort in buildings. The control logic is usually specified as ‘if-then-that-else’ rules that capture the domain expertise of HVAC operators, but they often have conflicts that may lead to sub-optimal HVAC performance. We propose EImprove, a reinforcement-learning (RL) based framework that exploits these conflicts to learn a resolution policy. We evaluate EImprove through a co-simulation strategy involving EnergyPlus simulations of a real-world office setting and a formal requirement specifier. Our experiments show that EImprove learns 75% faster than a pure RL framework.

Conventional automated test case generation techniques do not scale to modern software systems, as these systems have a large number of requirements that change frequently. In this paper, we present a scalable algorithm, AGenT, that generates test cases to cover maximal requirements. AGenT takes Expressive Decision Tables (EDT), specifying requirements of a system, as input and realises these as multiple Discrete Time Automata (DTAs). AGenT then generates test cases to cover each row of the tables. To improve scalability, it attempts to cover nearer rows (requiring fewer inputs) first, where distance is measured using a novel distance-to-match heuristic. It also maintains information about desirability and predictability of inputs so as to select promising inputs with a higher probability. Although the algorithm has been presented in the context of EDT, it operates on its DTA representation and hence can be applied to any system that is represented as a collection of DTAs like Statemate and Stateflow. In this paper, we describe AGenT in detail and present findings from two experiments that we conducted. We compared AGenT with state-of-the-art algorithms, DRAFT and a random test case generation algorithm, RTG. In the first experiment, AGenT took a maximum of 144 seconds to cover all rows whereas the other two algorithms timed out on many modules. In the second experiment, for a module with 701 rows, AGenT achieved 7% more coverage than DRAFT and 12% more than RTG.

Creating test cases to cover all functional requirements of real-world systems is hard, even for domain experts. Any method to generate functional test cases must have three attributes: (a) an easy-to-use formal notation to specify requirements, from a practitioner's point of view, (b) a scalable test-generation algorithm, and (c) coverage criteria that map to requirements. In this paper we present a method that has all these attributes. First, it includes Expressive Decision Table (EDT), a requirement specification notation designed to reduce translation efforts. Second, it implements a novel scalable row-guided random algorithm with fuzzing (RGRaF)(pronounced R-graph) to generate test cases. Finally, it implements two new coverage criteria targeted at requirements and requirement interactions. To evaluate our method, we conducted experiments on three real-world applications. In these experiments, RGRaF achieved better coverage than pure random test case generation. When compared with manual approach, our test cases subsumed all manual test cases and achieved up to 60% effort savings. More importantly, our test cases, when run on code, uncovered a bug in a post-production sub-system and captured three missing requirements in another.

Requirements of reactive systems express the relationship between sensors and actuators and are usually described in a natural language and a mix of state-based and stream-based paradigms. Translating these into a formal language is an important pre-requisite to automate the verification of requirements. The analysis effort required for the translation is a prime hurdle to formalization gaining acceptance among software engineers and testers. We present Expressive Decision Tables (EDT), a novel formal notation designed to reduce the translation efforts from both state-based and stream-based informal requirements. We have also built a tool, EDTTool, to generate test data and expected output from EDT specifications. In a case study consisting of more than 200 informal requirements of a real-life automotive application, translation of the informal requirements into EDT needed 43% lesser time than their translation into Statecharts. Further, we tested the Statecharts using test data generated by EDTTool from the corresponding EDT specifications. This testing detected one bug in a mature feature and exposed several missing requirements in another. The paper presents the EDT notation, comparison to other similar notations and the details of the case study.

Abstract interpretation is widely used to perform static code analysis with non-relational (interval) as well as relational (difference-bound matrices, polyhedral) domains. Analysis using non-relational domains is highly scalable but delivers imprecise results, whereas, use of relational domains produces precise results but does not scale up. We have developed a tool that implements K-limited path sensitive interval domain analysis to get precise results without losing on scalability. The tool was able to successfully analyse 10 million lines of embedded code for different properties such as division by zero, array index out of bound (AIOB), overflow-underflow and so on. This paper presents details of the tool and results of our experiments for detecting AIOB property. A comparison with the existing tools in the market demonstrates that our tool is more precise and scales better.

Static analysis of code is very effective in finding common programmer errors but it comes at a price - a large number of false positives. Model checking, on the other hand, is very precise but does not scale up. We have developed a tool that combines both techniques and also implements a novel loop abstraction. The tool was run on 2 million lines of embedded code to analyze for two properties - division by zero and array index out of bounds. In other experiments we compared the precision of our tool to that achieved by tools implementing abstract interpretation. This paper presents details of the tool and the results of evaluations that we have carried out to measure the scalability and to compare the precision of our method on industry code against other static analysis tools.

Visual notations like class diagrams, and use case diagrams are very popular with practitioners for capturing requirements of software applications. These notations unfortunately have little or no semantics, and hence cannot be analyzed by tools. Formal notations, on the other hand, have associated tools that check specifications for stated properties but are difficult to integrate with software development processes in use. Strengths of both approaches can be exploited by giving formal semantics to popular notations. Here we propose a novel usage of UML object diagrams for specifying pre- and post-conditions for use cases and capturing global system properties as class invariants. A translation is defined from object diagrams to the formal notation TLA/sup +/. The TLA/sup +/ specification is then formally verified using the model checker TLC. The proposed notation is intuitive, expressive and formal. We present a small case study to illustrate its strengths.