Slicing is a well-known program reduction technique where for a given program P and a variable of interest v at some statement P in the program, a program slice contains those set of statements belonging to P that affect v . This article presents two algorithms for interprocedural slicing of concurrent programs--a context-insensitive algorithm and a context-sensitive algorithm. The context-insensitive algorithm is efficient and correct (it includes every statement that may affect the slicing criterion) but is imprecise since it may include certain extra statements that are unnecessary. Precise slicing has been shown to be undecidable for concurrent programs. However, the context-sensitive algorithm computes correct and reasonably precise slices, but has a worst-case exponential-time complexity. Our context-sensitive algorithm computes a closure of dependencies while ensuring that statements sliced in each thread belong to a realizable path in that thread.A realizable path in a thread with procedure calls is one that reflects the fact that when a procedure finishes, execution returns to the site of the most recently executed call in that thread. One of the novelties of this article is a practical solution to determine whether a given set of statements in a thread may belong to a realizable path. This solution is precise even in the presence of recursion and long call chains in the flow graph.The slicing algorithms are applicable to concurrent programs with shared memory, interleaving semantics, explicit wait/notify synchronization and monitors. We first give a solution for a simple model of concurrency and later show how to extend the solution to the Java concurrency model. We have implemented the algorithms for Java bytecode and give experimental results.

Plug-n-Play style Intellectual Property (IP) reuse in System on Chip (SoC) design is facilitated by the use of an on-chip bus architecture. We present a synchronous, Finite State Machine based framework for modelling communication aspects of such architectures. This formalism has been developed via interaction with designers and the industry and is intuitive and lightweight. We have developed cycle accurate methods to formally specify protocol compatibility and component composition and show how our model can be used for compatibility verification, interface synthesis and model checking with automated specification. We demonstrate the utility of our framework by modelling the AMBA bus architecture including details such as pipelined operation, burst and split transfers, the AHB-APB bridge and arbitration features.

Verification of present day SoCs is proving to be challenging due to complex interactions among various subcomponents and IPs, with multiple clock domains and diverse bus protocols. The quality of verification depends on the precision in specifying the interaction behaviors. We propose a visual specification language called CESC (Clocked Event Sequence Chart), designed to specify interaction scenarios in SoCs. CESC provides a unique mechanism for representating multiple clock domains, based upon which event occurrences and interactions among different subcomponents can be represented. CESC has a pictorial and textual syntax, and a formal semantics to enable rigorous analysis. The semantics is based on standard notions of partial ordering and timed event traces. CESC is useful in many ways in formalizing SoC verification flows, namely, formalization of verification scenarios, synthesis of protocol checkers and consistency checking of specification versus implementation. This paper describes an algorithm to translate CESC scenarios to protocol checkers used in SoC verification flow. A few examples from industrial designs are included to illustrate the applicability of this formalism in specifying bus transactions and properties of protocols.

In this paper, we present two slicing tools: VHDL_Slice and Est_slice that compute static executable slices of VHDL and Esterel programs respectively. The slicers have been tested on a number of small and medium sized examples.

Automatic IP (Intellectual Property) matching is a key to reuse of IP cores. This paper presents an IP matching algorithm that can check whether a given programmable IP block can be adapted to match a given specification. When such adaptation is possible, the algorithm also generates a device driver to adapt the IP block. Though simulation, refinement and bisimulation based algorithms exist, they cannot be used to check the adaptability of an IP block, which is the essence of reuse. The IP matching algorithm is based on a formal verification technique called k-time forced simulation proposed in this paper k-time forced simulation may be used for identifying whether a given IP block (a device D) can be adapted to match a specification (a function F), given that D has a clock that is k-times faster than F. We demonstrate the applicability of the algorithm by reusing several IP blocks.

Synchronous languages may be used for specification and design of embedded systems. Assuming the availability of a library of synchronous programs, we propose a technique to enable reuse of these programs, via an algorithm for automatic matching of a design function to a program from the library. The algorithm, when successful, generates an interface which automatically adapts the program. The algorithm is based on a new simulation relation called synchronous forced simulation, which is shown to be necessary and sufficient for matching a given pair of function and program.

Component reuse techniques have been a recent focus of research because they are seen as the next-generation techniques to handle increasing system complexities. However, there are several unresolved issues to be addressed and prominent among them is the issue of component matching . As the number of reusable components in a component database grows, the task of manually matching a component to the user requirements becomes infeasible. Automating this matching can help in rapid system prototyping, improving quality and reducing cost. In addition, if the matching algorithm is sound, this approach can also reduce precious validation effort.In this article, we propose an algorithm for automatic matching of a design function to a device from a component database. The distinguishing feature of the algorithm is that when successful, it generates an interface that can automatically adapt the device to behave as the function. The algorithm is based on a new simulation relation called forced simulation that is shown to be a necessary and sufficient condition for component matching to be possible for a given pair of function and device. We demonstrate the application of the algorithm by reusing on some programmable components of the Intel family.

The object-oriented paradigm in software engineering provides support for the construction of modular and reusable program components and is attractive for the design of large and complex distributed systems. Reachability analysis is an important and well-known tool for static analysis of critical properties in concurrent programs, such as deadlock freedom. It involves the systematic enumeration of all possible global states of program execution and provides the same level of assurance for properties of the synchronization structure in concurrent programs, such as formal verification. However, direct application of traditional reachability analysis to concurrent object-oriented programs has many problems, such as incomplete analysis for reusable classes (not safe) and increased computational complexity (not efficient). We propose a novel technique called apportioning, for safe and efficient reachability analysis of concurrent object-oriented programs, that is based upon a simple but powerful idea of classification of program analysis points as local (having influence within a class) and global (having possible influence outside a class). We have developed a number of apportioning-based algorithms, having different degrees of safety and efficiency. We present the details of one of these algorithms, formally show its safety for an appropriate class of programs, and present experimental results to demonstrate its efficiency for various examples.

Slicing is a well-known program analysis technique for analyzing sequential programs and found useful in debugging, testing and reverse engineering. This paper extends the notion of slicing to concurrent programs with shared memory, interleaving semantics and mutual exclusion. Interference among concurrent threads or processes complicates the computation of slices of concurrent programs. Further, unlike slicing of sequential programs, a slicing algorithm for concurrent programs needs to differentiate between loop-independent data dependence and certain loop-carried data dependences.

The object-oriented paradigm has been found to be useful for the construction of large and complex concurrent systems. Reachability analysis is an important and well-known tool for static (pre-run-time) analysis of concurrent programs. However, direct application of traditional reachability analysis to concurrent object-oriented programs has many problems, such as incomplete analysis for reusable classes (not safe) and increased computational complexity (not efficient). We have proposed a novel technique called apportioning, for effective reachability analysis of concurrent object-oriented programs, that integrates the techniques of abstraction (considering a reduced representation of the system) and partitioning (dividing the system into smaller units). The given program is apportioned into a reduced version of each of its classes, as well as a reduced version of the program. The error to be checked is also decomposed into appropriate sub-properties for checking in the reachability graphs corresponding to the apportioned program. We have developed a number of apportioning-based algorithms, having different degrees of safety and effectiveness. In this paper, we present the details of one of these algorithms.

The task of designing large real-time reactive systems, which interact continuously with their environment and exhibit concurrency properties, is a challenging one. The authors explore the utility of a combination of behavior and function specification languages in specifying such systems and verifying their properties. An existing specification language, statecharts, is used to specify the behavior of real-time reactive systems, while a new logic-based language called FNLOG (based on first-order predicate calculus and temporal logic) is designed to express the system functions over real time. Two types of system properties, intrinsic and structural, are proposed. It is shown that both types of system properties are expressible in FNLOG and may be verified by logical deduction, and also hold for the corresponding behavior specification.

The object-oriented paradigm provides support for modular and reusable design and is attractive for the construction of large and complex concurrent systems. Reachability analysis is an important and well-known tool for static (pre-run-time) analysis of concurrent programs. However its direct application to concurrent object-oriented programs has many problems, such as incomplete analysis for reusable classes and increased computational complexity. It also seems impossible to arrive at a single general-purpose strategy that is both safe and effective for all programs. The authors propose a tool-suite based approach for the reachability analysis of concurrent object-oriented-programs. This approach enables choice of an appropriate 'ideal' tool, for the given program and also provides the flexibility for incorporation of additional tools. They have also proposed a novel abstraction-based partitioning methodology for effective reachability analysis of concurrent object-oriented programs. Using this methodology, they have developed a variety of tools, having different degrees of safety, effectiveness and efficiency, for incorporation into the tool-suite. They have formally shown the safety of these tools for appropriate classes of programs and have evaluated their effectiveness and efficiency.

Canonical Completion of a poset is of central importance in obtaining fully abstract semantic models. Stoughton, in his thesis, has described a completion technique. In this short note, we provide a direct characterization of the cpo constructed using this technique. This characterization shows that the completed poset consists of all closed continuously directed subsets of the original poset and vice versa. This result is stated as a conjecture by Stoughton.

We present a new programming paradigm called Communicating Reactive Processes or CRP that unifies the capabilities of asynchronous and synchronous concurrent programming languages. Asynchronous languages such as CSP, Occam, or Ada are well-suited for distributed algorithms; their processes are loosely coupled and communication takes time. The Esterel synchronous language is dedicated to reactive systems; its processes are tightly coupled and deterministic, communication being realized by instantaneous broadcasting. Complex applications such as process or robot control require to couple both forms of concurrency, which is the object of CRP. A CRP program consists of independent locally reactive Esterel nodes that communicate with each other by CSP rendezvous. CRP faithfully extends both Esterel and CSP and adds new possibilities such as precise local watchdogs on rendezvous. We present the design of CRP, its semantics, a translation into classical process calculi for program verificatio...