Testing PLC and DCS control logic in industrial automation is laborious and challenging since appropriate test cases are often complex and difficult to formulate. Researchers have previously proposed several automated test case generation approaches for PLC software applying symbolic execution and search-based techniques. Often requiring formal specifications and performing a mechanical analysis of programs, these approaches may uncover specific programming errors but some-times suffer from state space explosion and cannot process rather informal specifications. We proposed a novel approach for the automatic generation of PLC test cases that queries a Large Language Model (LLM) to synthesize test cases for code provided in a prompt. Experiments with ten open-source function blocks from the OSCAT automation library showed that the approach is fast, easy to use, and can yield test cases with high statement coverage for low-to-medium complex programs. However, we also found that LLM-generated test cases suffer from erroneous assertions in many cases, which still require manual adaption.

The Architecture Analysis and Design Language (AADL) is a rich language for modeling embedded systems through several constructs such as component extension and refinement to promote modularity of component declarations. To ease processing AADL models, OSATE, the reference tool for AADL, defines another model (namely 'instance' model) computed from a base 'declarative' model/s. An instance model is a simple object tree where all information from the declarative model is flattened so that tools can easily use this information to analyze the system. However for modifications, they have to make changes in the complex declarative model since there is no automated backward transformation (deinstantiation) from instance to declarative models. Since the instance model is a 'view' of the declarative model, this is a view-update problem. In this paper, we propose the OSATE Declarative-Instance Mapping Tool (OSATE-DIM1), an Eclipse plugin for deinstantiation of AADL models implementing a solution of this view-update problem. We evaluate OSATE-DIM with a benchmark of existing AADL model processing tools and verify the correctness of our deinstantiation transformations. We also discuss how our approach could be useful for decompilation of Object-Oriented languages' intermediate representations.

Software for embedded systems goes through a scheduling phase where it is subjected to optimizing transformations. In such a scenario, validating the preservation of semantics across the transformation is essential. In this paper, we present PNPEq (Petri Net Program Equivalence), an ongoing work on a novel translation validation technique to handle various schedule-time conditional optimizations among others. The method makes use of a reduced size Petri net model integrating SMT solvers for validating arithmetic transformations. The approach is illustrated with a simple program and its translation, and further validated with a preliminary example suite.

Evaluation of descriptive type questions automatically is an important problem. In this paper, we have concentrated on programing language course which is a core subject in CS discipline. In this paper, we have given a tool prototype which evaluates the descriptive type of questions in computer programing course using the notion of program equivalence.

The initial behavioural specification of any software programs goes through significant optimizing and parallelizing transformations, automated and also human guided, before being mapped to an architecture. Establishing validity of these transformations is crucial to ensure that they preserve the original behaviour. PRES+ model (Petri net based Representation of Embedded Systems) encompassing data processing is used to model parallel behaviours. Being value based with inherent scope of capturing parallelism, PRES+ models depict such data dependencies more directly; accordingly, they are likely to be more convenient as the intermediate representations (IRs) of both the source and the transformed codes for translation validation than strictly sequential variable-based IRs like Finite State Machines with Data path (FSMDs) (which are essentially sequential control flow graphs (CFGs)). In this work, a path based equivalence checking method for PRES+ models is presented.