Search

This special issue of Software Tools for Technology Transfer presents extended versions of two selected papers from the 23rd edition of TACAS, the International Conference on Tools and Algorithms for the Construction and Analysis of Systems that took place in April 2017 in Uppsala. The papers included in this special issue concern various aspects of automated design and formal verification; they therefore contribute to the development of more reliable computer systems. [ABSTRACT FROM AUTHOR]

Design by contract (DbC) is a software development methodology that focuses on clearly defining the interfaces between components to produce better quality object-oriented software. Though there exists ample support for DbC for sequential programs, applying DbC to concurrent programs presents several challenges. Using Java as the target programming language, we tackle such challenges by augmenting the Java Modelling Language (JML) and modifying the JML compiler (jmlc) to generate runtime assertion checking code to support DbC in concurrent programs. We applied our solution in a carefully designed case study on a highly concurrent industrial software system from the telecommunications domain to assess the effectiveness of contracts as test oracles in detecting and diagnosing functional faults in concurrent software. Based on these results, clear and objective requirements are defined for contracts to be effective test oracles for concurrent programs whilst balancing the effort to design them. Effort is measured indirectly through the contract complexity measure (CCM), a measure we define. Main results include that contracts of a realistic level of completeness and complexity can detect around 76 percent of faults and reduce the diagnosis effort for such faults tenfold. We, therefore, show that DbC can be applied to concurrent software and can be a valuable tool to improve the economics of software engineering. [ABSTRACT FROM PUBLISHER]

For protecting an intellectual property (IP) core, it must be harder to reverse engineer. Structural obfuscation can play an important role in achieving this goal. A novel structural obfuscation methodology during architectural synthesis using multiple compiler‐based high‐level transformations (HLTs) that yield functionally equivalent designs (data flow graphs) which are camouflaged in identity is proposed. The proposed obfuscation methodology is driven through a number of HLT techniques such as redundant operation elimination, logic transformation and tree height transformation. In addition to performing obfuscation, performing area–delay tradeoff during exploring low‐cost obfuscated design is also possible using these HLT techniques in the proposed methodology. Owing to multiple stages of HLT incorporated in the proposed approach during obfuscation, it yields a highly robust design which on integration with particle swarm optimisation‐based exploration framework produced low‐cost obfuscated IP designs. Results of the proposed approach yielded an enhancement in strength of obfuscation of 20.19% and reduction in obfuscated design cost of 59.66% compared with a similar approach. [ABSTRACT FROM AUTHOR]

In this paper, we present a technique for compact representation of execution sequences in terms of efficient looping constructs. Here, by a looping construct, we mean a compact way of specifying a finite repetition of a set of execution primitives. Such compaction, which can be viewed as a form of hierarchical run-length encoding (RLE), has application in many very large scale integration (VLSI) signal processing contexts, including efficient control generation for Kahn processes on field-programmable gate arrays (FPGAs), and software synthesis for static dataflow models of computation. In this paper, we significantly generalize previous models for loop-based code compaction of digital signal processing (DSP) programs to yield a configurable code compression methodology that exhibits a broad range of achievable tradeoffs. Specifically, we formally develop and apply to DSP hardware and software synthesis a parameterizable loop scheduling approach with compact format, dynamic reconfigurability, and low-overhead decompression. [ABSTRACT FROM AUTHOR]