Symbolic execution is an important program analysistechnique that has found a number of applications in the last fifteen years or so.Popular symbolic execution approaches use backtracking when faced with infeasibility along a path being explored.A simple backtracking strategy (i.e.backtracking by a single decision node) may suffice when the goal is to cover the entire control flow graph (CFG).However, if the goal is to cover specific parts of the CFG through a single path, simple backtracking may lead to non-optimality or even non-termination.In this paper, we present weighted backtracking strategy (WBS) that exploits previous knowledge about the program behaviour to compute 'good' candidates as destinations of backtracking.We have integrated our heuristic to SymTest, a symbolic testing framework for embedded systems.Experiments with casestudies have demonstrated that WBS improves SymTest's performance both in its ability to achieve termination as well as in computing shorter test sequences compared to the original approach.SymTest with WBS generates shorter test sequences compared to several other existing test generation approaches based on symbolic execution.

The updating and upgrading of control systems is a cumbersome, expensive and time consuming task. From a software perspective, control system migration is a collective task of migrating the control logic, Human Machine Interface (HMI) and auxiliary software applications. Migrating control logic is the most challenging task owing to constraints on hard real-time behavior and execution order. Control logic typically contains engineering artifacts that specify the functionality of industrial devices taking into account various parameters. Therefore, to migrate from one Distributed Control System (DCS) system to another or to upgrade the existing DCS, one needs to map the source control entity and their parameters to the appropriate control entities in the target DCS.In this paper, we propose a machine learning based suggestion management system that identifies control entities and parameters for a source DCS and suggests the use of similar control entities and corresponding parameters for the target DCS. This in effect saves effort required in mapping of control parameters and reduces the dependence on subject matter experts. Our system uses a probabilistic approach to find these similarity mappings based on meta-data stored in an Ontology. We further describe a case study implemented for mapping heritage and legacy systems to a modern control system to verify and validate our approach.

Automated testing tools for programs written in IEC 61131-3 standard of programming languages supporting the development of PLC control software is less available. Symbolic execution is a program analysis technique that determines what inputs cause each part of a program to execute. Here, a symbolic execution framework is utilized to achieve test target coverage for control system software. The framework does not ensure optimal feasible paths after backtracking. In this paper an approach using weight calculation is utilized to overcome the drawback. The calculated weight values helps to backtrack to a node, on flipping will result in an optimal feasible path.

Test suite minimization ensures that an optimum set of test cases are selected to provide maximum coverage of requirements. In this paper, we discuss and evaluate techniques for test suite minimization of evolving software systems. As a case study, we have used an industrial tool, Static Code Analysis (SCAN) tool for Electronic Device Description Language (EDDL) as the System Under Test (SUT). We have used standard approaches including Greedy, Greedy Essential (GE) and Greedy Redundant Essential (GRE) for minimization of the test suite for a given set of requirements of the SUT. Further, we have proposed and implemented k-coverage variants of these approaches. The minimized test suite which is obtained as a result reduces testing effort and time during regression testing. The paper also addresses the need for choosing an appropriate level of granularity of requirements to efficiently cover all requirements. The paper demonstrates how fine grained requirements help in finding an optimal test suite to completely address the requirements and also help in detecting bugs in each version of the software. Finally, the results from different analyses have been presented and compared and it has been observed that GE heuristics performs the best (run time) under certain conditions. Copyright © 2019 by SCITEPRESS - Science and Technology Publications, Lda. All rights reserved.

In recent times, there has been significant interest in collaborative robots where the tasks performed by a robot are non-repetitive and complex, and humans and robots share an overlapping workspace. In such a case, the robot controller must necessarily be safety-aware. In this paper, we propose a mechanism to evaluate a robot program and compute a safety score for each action that the robot is about to perform. To this end, we have implemented a code analyzer that examines the robot's Move instructions and assigns a safety score. A subjective logic based approach is used to compute the safety score for each instruction. We have evaluated the approach through ABB's RobotStudio®simulator. We simulate two scenarios: First, where two robots share a workspace and second, where a robot moves along a path with an obstacle. The simulations show that using our code analyzer and safety score formalism; it is possible to evaluate the application code for safety and enable avoidance of potentially unsafe behavior.

Software used to monitor and control operations within an automation system is defined using domain-specific languages. Latent errors in the control code, if left undetected, can lead to unexpected system failures compromising the safety and the security of the automation system. Traditional analysis techniques are insufficient to detect such errors as they do not cater specifically to the underlying domain-specific language. However, given the diversity of different automation domains, there is no standard platform for analysis of these languages. This paper proposes a generic static analysis framework for domain-specific languages used in the automation domain. The analysis approach exhaustively detects runtime errors in control code and ensures compliance to good programming practices. These runtime errors and coding violations are checked against abstract syntax trees and control flow graphs derived from the code. Data Flow Analysis (DFA), Abstract interpretation and pattern-based matching techniques are used to identify domain specific errors and coding violations for control languages.

Renewables play an important role in today's sustainable power and energy systems. In this paper, we model and analyze an FPGA based power management system for renewables by using the UPPAAL modeling and verification tool. Our main objective is to ensure correctness of the system design using formal methods based techniques. Through our case study, we establish the correctness of the FPGA based control algorithm with respect to the system requirements. All requirements regarding effective utilization of loads and sources by their activation and deactivation, and also requirements of battery bank (which ensures that battery will not charge and discharge deeply), are specified using Timed Computation Tree logic. On the basis of our analysis, we confirm that the design of the implemented power management system conforms to its specifications.

Abstract Developers often migrate their applications to support various platform/programming‐language application programming interfaces (APIs) to retain existing users and to attract new users. To migrate an application written using 1 API (source) to another API (target), a developer must know how the methods in the source API map to the methods in the target API. Given that a typical platform or language exposes a large number of API methods, manually discovering API mappings is prohibitively resource‐intensive and may be error prone. The goal of this research is to support software developers in migrating an application from a source API to a target API by automatically discovering relevant method mappings across APIs using text mining on the natural language API method descriptions. This paper proposes text mining based approach (TMAP) to discover relevant API mappings. To evaluate our approach, we used TMAP to discover API mappings for 15 classes across (1)JavaandC#API; and (2)Java MEandAndroidAPI. We compared the discovered mappings with state‐of‐the‐art source code analysis‐based approaches: Rosetta and StaMiner. Our results indicate that TMAP on average found relevant mappings for 56% and 57% more methods compared to the Rosetta and the StaMiner approaches, respectively.

Prevention of data loss in each scan cycle is of utmost importance in control system programming. For each variable to reflect the latest value, compilers compute the order of execution of control logic objects according to data flow. But this technique for ensuring data integrity fails when a circular dependency or a “code loop” is found. In this paper, we propose an approach to help solve this issue in 2 steps - by providing an interactive visual representation and providing a list of possible solutions. A tool is implemented based on this approach which can take either the control logic code or the dump created by the compiler as input. The tool has been validated for effectiveness with industrial use cases from different domains.

Developers often release different versions of their applications to support various platform/programming-language application programming interfaces (APIs). To migrate an application written using one API (source) to another API (target), a developer must know how the methods in the source API map to the methods in the target API. Given a typical platform or language exposes a large number of API methods, manually writing API mappings is prohibitively resource-intensive and may be error prone. Recently, researchers proposed to automate the mapping process by mining API mappings from existing code-bases. However, these approaches require as input a manually ported (or at least functionally similar) code across source and target APIs. To address the shortcoming, this paper proposes TMAP: Text Mining based approach to discover likely API mappings using the similarity in the textual description of the source and target API documents. To evaluate our approach, we used TMAP to discover API mappings for 15 classes across: 1) Java and C# API, and 2) Java ME and Android API. We compared the discovered mappings with state-of-the-art source code analysis based approaches: Rosetta and StaMiner. Our results indicate that TMAP on average found relevant mappings for 57% more methods compared to previous approaches. Furthermore, our results also indicate that TMAP on average found exact mappings for 6.5 more methods per class with a maximum of 21 additional exact mappings for a single class as compared to previous approaches.

Latent errors in control system software can be hard to detect through traditional testing techniques. Such errors, if left undetected, could manifest themselves as failures during run-time that could be potentially catastrophic and very expensive to fix. In this paper, we present a static code analysis approach to detect potential sources of such run-time errors during compile time itself, thus ensuring easy identification, safe execution and reducing the effort required during debugging. In order to detect run-time errors, the control system application is first parsed to generate a set of abstract syntax trees, which in turn are used to derive the control flow graph for the application. A hybrid algorithm, based on abstract interpretation and traditional data flow analysis techniques is used to check the control flow graph for type constraints, reachability and liveness properties. Additionally, the abstract syntax trees are used to check for datatype mismatches and compliance violations. A proof of concept prototype is implemented to demonstrate how the algorithm/approach can be used to analyze control applications developed using domain specific languages such as those complying with the IEC 61131-3 standard.

Our experiences with industrial software development projects have often revealed that requirements change even after their formal approvals. Although the requirements are never stable, proactive identification of potentially changeable or deferrable requirements, and estimation of their impacts early in a project can be useful in minimizing the risks and cost overruns. In practice, the decisions to change or defer certain requirements are based on experience, and are mostly driven by business needs and product release timelines. There are no techniques available which could foresee such changes early in the project. In this work, we perform exploratory analysis of the requirement artifacts from thirty three industrial software development projects and shared our observations on different requirement change attributes. Through empirical analysis, we evolve the relative weights of each of these attributes in terms of their impacts on the project schedule and effort. Based on the analysis, a model is developed to predict the impact due to requirement changes and it is validated. This model can be used to develop a requirement change decision support tool to assist decision makers.

IEC 61131-3 is an open standard that provides guidelines for programmable logic controllers and control systems. The standard defines specifications for control system programming languages, both textual and graphical. A control system application developed using these languages can go through several changes over the course of the project's life-cycle. While differences in textual programs can be detected using traditional text difference algorithms, there exist no effective means for tracking changes at a granular, semantic level for graphical control system programs. In this paper, we present an approach for comparison of graphical IEC 61131-3 programs, specifically those written using the Function Block Diagram and Sequential Function Chart notations. To perform this comparison, we represent the programs in an XML format, and use this to compare individual elements. The differences are computed and the programs are then rendered in a customized graphical viewer that highlights changes between programs. We implement a prototype comparison utility for graphical IEC 61131-3 programs and show how it can help reduce the effort involved in manual review and maintenance activities.

In order to maximize cost and quality gains, industrial automation systems need to incorporate the best practices of software engineering in their application development process. However, this requires the right set of tools and methodologies that cater to the needs of the automation domain. While there have been a few efforts towards applying state-of-the-art software engineering tools and techniques to the automation domain, these have not been universally adopted. This paper discusses some of the challenges in adopting software engineering principles for industrial automation application development. Further, the paper presents a case for research activities to look for more practical solutions for industrial applications.

This paper presents our effort of using model-driven engineering to establish a safety-assured implementation of Patient-Controlled Analgesic (PCA) infusion pump software based on the generic PCA reference model provided by the U.S. Food and Drug Administration (FDA). The reference model was first translated into a network of timed automata using the UPPAAL tool. Its safety properties were then assured according to the set of generic safety requirements also provided by the FDA. Once the safety of the reference model was established, we applied the TIMES tool to automatically generate platform-independent code as its preliminary implementation. The code was then equipped with auxiliary facilities to interface with pump hardware and deployed onto a real PCA pump. Experiments show that the code worked correctly and effectively with the real pump. To assure that the code does not introduce any violation of the safety requirements, we also developed a testbed to check the consistency between the reference model and the code through conformance testing. Challenges encountered and lessons learned during our work are also discussed in this paper.

New research is underway at the FDA to investigate the benefits of integrating architecture analysis into safety evaluations of medical-device software. Due to the complexity in setting up testing environments for such software, the FDA is unable to conduct large-scale safety testing, instead, it must rely on other techniques to build an argument for whether the software is safe or not. The architecture analysis approach, formalized using relational algebra, is based on reconstructing abstract, yet precise, architectural views from source code to help build such arguments about safety. This paper discusses the use of the formal approach to analyze the Computer-Assisted Resuscitation Algorithm (CARA) software, which controls an infusion pump designed to provide automated assistance for transfusing blood. The results suggest that a) architecture analysis offers many insights related to software quality in general and testability (i.e., the ease of testing) and its impact on safety in particular, and b) architectural analysis results can be used to help configure static analysis tools to improve their performance for verifying safety properties.

In this paper we explore a method for carrying out pre-market analysis of software designs and implementations, based on formal-methods techniques, to aid the process of reviewing software in medical devices. We discuss a methodology to validate medical device software with the help of formal methods based usage models, and test cases derived from such models. We present a case study involving the design and verification of a generic infusion pump usage model, detailing how the various stages of our approach can be carried out. Finally, we present experimental results and effort estimates to show that the proposed methodology is effective and feasible

Post-mortem analysis - the process of tracing software failure to source code - is an important means for maintenance engineers and regulatory reviewers for establishing the cause of an error. Historically, static slicing techniques have been used for aiding post-mortem fault analysis. However, the slices obtained in this manner can often be too large and may not give a clear understanding of the code when dealing with complex reactive systems. We propose using model abstraction in conjunction with slicing to ameliorate the problem of understanding large slices. Combining slicing with abstraction provides the analyst with an integrated cognition model, leading to a better understanding of the code, and consequently more efficient error analysis. We formalize this concept through the notion of abstraction-driven slicing, and use it to develop CAdS, an automated tool to aid postmortem error detection in C programs using abstraction-driven static slicing. We list our experiences with CAdS and illustrate how it can be used to reduce effort involved in the postmortem analysis process