Role-based Access Control (RBAC) is one of the most widely implemented access control models. In today's complex computing systems, one of the increasingly sought-after features for reliable security is information flow control. Although RBAC is a policy-neutral and generic model, its implementations generally do not provide information flow control. In this paper, we present two approaches to address this issue. In the first method, we describe how a lattice model can be captured using an RBAC configuration. In the second method, we analyze the information flows in a given RBAC policy using a decentralized lattice model called Readers-Writers Flow Model. This method identifies the indirect information flows in the policy and helps in creating flow-secure RBAC policies. We discuss the scope and limitations of these methods in detail and also present a brief case study. Finally, we investigate the use of flow-secure RBAC policies in creating flow-secure Attribute-based Access Control (ABAC) policies.

For the last two decades, a wide spectrum of interpretations of non-interference11The notion of non-interference discussed in this paper enforces flow security in a program and is different from the concept of non-interference used for establishing functional correctness of parallel programs [1] have been used in the security analysis of programs, starting with the notion proposed by Goguen & Meseguer along with arguments of its impact on security practice. While the majority of works deal with sequential programs, several researchers have extended the notion of non-interference to enforce information flow-security in non-deterministic and concurrent programs. Major efforts of generalizations are based on (i) considering input sequences as a basic unit for input/output with semantic interpretation on a two-point information flow lattice, or (ii) typing of expressions as values for reading and writing, or (iii) typing of expressions along with its limited effects. Such approaches have limited compositionality and, thus, pose issues while extending these notions for concurrent programs. Further, in a general multi-point lattice, the notion of a public observer (or attacker) is not unique as it depends on the level of the attacker and the one attacked. In this paper, we first propose a compositional variant of non-interference for sequential systems that follow a general information flow lattice and place it in the context of earlier definitions of non-interference. We show that such an extension leads to the capturing of violations of information flow security in a concrete setting of a sequential language. Finally, we generalize non-interference for concurrent programs and illustrate its use for security analysis, particularly in the cases where information is transmitted through shared variables.

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.

Summary In this paper, we propose an enhanced Automatic Checkpointing and Partial Rollback (CaPR++) algorithm to realize Software Transactional Memory (STM), that employs partial rollback mechanism for conflict resolution. We have comparatively evaluated the “Abort” and “Partial Rollback” mechanisms for STMs. For purposes of comparison, we have used the state‐of‐the‐art RSTM system and for the “Partial Rollback”, and we have used our earlier CaPR+ algorithm that has been enhanced for our requirements. Note that we have enriched the STAMP benchmarks with varied delayed transaction times. The results obtained demonstrate the effectiveness of the Partial Rollback mechanism over pure abort mechanisms for applications consisting of large transaction delays, with up to 1.6x performance gain for applications with large transactional delays. Our study makes the case for a hybrid system of pure aborts and partial rollbacks, which can extract the benefits of both mechanisms. Keeping in line with our study, we have proposed a hybrid implementation where some of the transactions of an application subscribe to abort mechanisms and the rest to partial rollback. Our initial implementation demonstrates various scenarios where the hybrid approach outperforms the pure abort and partial rollback approaches.

Summary Graphics Processing Units (GPUs) have evolved from pure graphics applications toward general purpose applications, often referred to as GPGPU computing. However, its scope is still limited to data‐parallel applications that require little synchronization. As synchronization on GPUs is quite costly, synchronization requirements in GPUs are usually realized using existing synchronization primitives like atomic operations and barriers. These approaches either incur significant overhead or place certain restrictions in their usage, affecting the scalability/scope of such applications. The lack of adequate support for fine‐grained synchronization has restricted the realization of irregular algorithms on GPUs, wherein control flow and memory access patterns are data‐dependent and unpredictable. Recently, there has been an interest in building relationship between lock‐step semantics and interleaving semantics and to develop lock‐based synchronization mechanism for GPUs to overcome these issues. GPUs follow SIMD, and hence, when adapted for general purpose computing, new distinct deadlock scenarios arise. In this paper, we discuss various deadlock scenarios that can happen in GPUs, and present a modeling of deadlocks in GPUs. We shall first illustrate such deadlock scenarios in GPU applications, and then describe a novel lock‐based deadlock‐free, fine‐grained synchronization mechanism for GPU architectures that overcomes deadlocks without a significant overhead. We further establish the correctness of our methods and discuss the performance overheads.

Several approaches to protect data and code, and ensure execution in a secure environment without getting infected from malwares, such as isolation, sandboxing, trust-based execution, application oriented access control have been proposed. In recent times, hardware-based solutions like ARM TrustZone and Intel SGX Enclave have been introduced to protect code and data from being infected or modified from outside the designated “secure” zone. While the hardware-based approaches have a distinct advantage, they have disadvantages in realizing Multi-Level Secure (MLS) systems, as they need to communicate via a central agent; further, a software vault would provide a good alternative when a system (like smartphone) is used/owned by a single person. In this paper, we describe a general approach for the creation of a software vault to preserve integrity and confidentiality of the information and computation end-to-end while supporting inter-communication among different components. This realizes an efficient interacting system that is secure and as good as the system using the hardware-based solutions. Our solution is through dynamic labelling using the recent information flow models for decentralized systems. We illustrate the application of our technique for building a runtime monitor for the Android environment, and demonstrate its characteristic properties by realizing a secure banking application. The solution guarantees end-to-end preservation of confidentiality & integrity, and allowing interactions among distributed components but still preserving the hardness of penetration from malware. We believe that our software vault will have extensive applications in utility computing that demands inter-communication between clouds.

Security protocols are essential for establishing trustworthiness of electronic transactions over open networks. Currently used languages and logics for protocol specifications do not facilitate/force the designer to make explicit goals, intentional assumptions or the preceding history across interactions among the stakeholders. Readers-Writers Flow Model (RWFM) is a novel model for information flow control, and has a label structure that explicitly specifies the permissible readers and influencers of a message. RWFM labels succinctly capture the history of a message. In this paper, we sketch an approach to enrich protocol specifications with RWFM labels that overcomes the problem of incomplete protocol specifications, and captures the intensional specifications in a natural way. Our approach tracks information flows in a protocol and makes explicit: (i) the assumptions and goals at each stage of the protocol, (ii) the construction of new messages from components of previous messages, and (iii) the knowledge of roles at various stages. We believe that our approach leads to a robust protocol specification language, including security/cryptographic protocols, that shall be of immense aid to the designer, user and the implementer of protocols.

Lattice model of secure information flow (referred as LIFS) is the foundation for building secure systems. In this paper, we capture the lattice model of security for mobility in a distributed setup using the formalism of Mobile Ambient calculus (MA) that has been widely used to model mobility and concurrency. Our model, referred to as Labelled Mobile Ambients (LMA), assigns labels to ambients for tracking information flow in the system, and provides semantics for preserving the distributed information flow policy specified by the labels. While there exist variants of the mobile ambient calculus for modelling application specific aspects of mandatory access control like confidentiality and integrity in the literature, our LMA model subsumes these models by capturing confidentiality and integrity as special cases of information flow properties. Thus, the LMA model enables a wide range of applications with complex security requirements, and permits a simple static analysis to establish whether the system violates information flow policy. A relative comparison to other prominent works is provided highlighting the merits of our LMA.

Due to technological advances, it has been a common practice for quite some time to use embedded computers for the monitoring and control of physical processes/plants. These are essentially networked computer-based systems consisting of application-specific control-processing systems, actuators, sensors etc., used for digitally controlling physical systems (often in a federated manner) within a defined geographical location such as power plants, chemical plants etc. Different terminologies like distributed control systems (DCS), cyber-physical systems (CPS), supervisory control and data acquisition systems(SCADA) etc., are used to denoting similar usage. Technology has further made it possible to federate/ integrate heterogeneous (even built by different manufacturers) systems. While such capabilities have provided the needed flexibility and user convenience, it has also created challenges for system designers not only from the correctness point of view but also from the point of view of security and protection of the underlying physical plants. With the arrival of complex malwares, it has become very challenging to secure network and information systems from intruders and protect the systems from attackers. Recently, complex malwares like Stuxnet, Flame etc., have specifically targeted SCADA of public infrastructures like power grids/plants, and thus, bringing to the forefront the challenges in securing and protecting SCADA. The above mentioned malwares are horrendously complex and hence, need a wholesome approach for detection and protection. In these scenarios, apart from the classical IT security, there is a need to look at other plausible new attacks considering the domain of the physical systems in conjunction with the capabilities of the embedded computers, and arrive at methods of protection and risk evaluation.

BPMN is widely used in Model Drive Architectures (MDA) for enterprise-scale solutions. In this paper, we shall realize an executional platform for MDA framework using BPMN. We transform BPMN into an executional framework using Orc [1]. Orc is a web orchestration language that provides uniform access to computational services, including distributed communication and data manipulation. The interesting features of Orc are its capability to specify patterns like multi-merge, discriminator, arbitrary cycles, several multiple instances etc. cleanly. It supports the realization of the map-reduce paradigm for distributed computing and thus, provides a powerful MDA approach for business analysts to express their solutions. It will enable creation/simulation of mock scenarios and the use of verification/validation/debugging in an integrated way. In this paper, we describe a transformation of BPMN core elements to Orc. We use a graph based approach where a Business Process Diagram(BPD) diagram is validated and then converted to a set of Orc computation structures. We describe the transformations along with an implementation and illustrate the process with an example.

The distributed nature of web services, absence of a single stakeholder and the resulting fact that there is no control on the individual web services makes it difficult to ensure that the computation underlying the web service composition proceeds as intended. Thus, it is essential to monitor the computations at runtime to satisfy the needs of the user safety and QoS properties. In this paper, we describe the design and development of a runtime monitor which executes concurrently with the runtime system of a web service orchestration language. The monitoring property, is specified either as wanted/unwanted scenarios or specified as a formula using a subset of temporal logic called SL. From the given properties, we derive the observers as reactive automata using a synchronous framework and integrate them with the underlying engine of the web service specification language, for our implementation, we have used Orc. We illustrate our implementation through examples of monitoring various web service properties.

Malicious code is any code that has been modified with the intention of harming its usage or the user. Typical categories of malicious code include Trojan Horses, viruses, worms etc. With the growth in complexity of computing systems, detection of malicious code is becoming horrendously complex. For security of embedded devices it is important to ensure the integrity of software running in it. The general virus detection is undecidable. However, in the case of embedded systems or personal systems, the software and hardware configurations are known a priori. We are experimenting to see whether we can certify such systems for malware freedom. Most of the current efforts on malware detection rely heavily on detection of syntactic patterns. Malware writers are resorting to simple syntactic transformations (which preserve the program semantics) such as various compiler optimizations and program obfuscation techniques to evade detection. Our work is based on semantic behaviour of programs. We are working towards developing a model of the behaviour of a program executing in an environment. Our approach to detect tampering is based on benchmarking the behaviour of a program executing in an environment, and then matching the observed behaviour of the program in a similar environment with the benchmark (a la translation validation in a sense or bisimulation that is widely used in model checking). Since execution behaviour remains the same in majority of obfuscations, our approach is resilient to such exploits. We have performed several experiments in this direction and obtained encouraging results. Differences between the benchmarked behaviour and the observed behaviour quantifies the damage due to a virus. This enables us to arrive at refined notions of "harm" done by a virus and appropriate measures for protection.

Static single assignment (SSA) form has been widely studied and used for sequential programs. This form enables many compiler optimizations to be done efficiently. Work on concurrent static single assignment form (CSSA) for concurrent programs is focused on languages that have limited, implicit barriers (e.g., cobegin/coend and parallel do). Recent programming languages for high-performance computing have general features for barrier/phase synchronization - this is essentially a dual of mutual exclusion and arises mainly in constructing synchronous systems from asynchronous systems. X10 is one such language that has features for general purpose barriers. In X10, barriers are provided through features such as clocks and finish. Since barriers provide explicit synchronization, they offer an opportunity for reducing pi interferences needed for CSSA. This paper provides a means for computing improved CSSA form of a program taking advantage of the general barriers present in it. Our algorithm is based on constructing a control-flow graph of the program and flow equations. The efficiency of analysis and optimizations for parallel programs depends on the number and complexity of pi assignments in their CSSA representations. We demonstrate that our approach of computing CSSA form for languages supporting general barrier synchronization can improve the precision of intermediate representation for computing global value numbering and loop invariant detection.

General barrier synchronization is widely used in multiprocessor programming with the introduction of multicore processors. In this paper, we describe a solution for the barrier synchronization of processes (that are not bounded or known a priori) that can dynamically join or drop out of barrier synchronization. A new process can join only in the beginning of each phase along with all the other members; that is, at the beginning of a phase everyone is aware of the other members involved in synchronization. We design a protocol using the above policy that guarantees starvation freedom, i.e., any process wanting to join phase synchronization shall do so within at most two phases.

We present a novel, table-free technique for detecting all temporal and spatial memory access errors (e.g. dangling pointers, out-of-bounds check, etc.) in programs supporting general pointers. Our approach is the first technique to provide such error checking using only constant-time operations. The scheme relies on fat pointers, whose size is contained within standard scalar sizes (up to two words) so that atomic hardware support for operations upon the pointers is obtained along with meaningful casts in-between pointers and other scalars. Optimized compilation of code becomes possible since the scalarized-for-free encoded pointers get register allocated and manipulated. Backward compatibility is enabled by the scalar pointer sizes, with novel automatic support provided for encoding and decoding of fat pointers in place for interaction with unprotected code (e.g. library binaries). Implementation and benchmarks of the technique over several applications of the memory-intensive Olden suite indicate that the average time overhead of our method is about half the time cost of an unprotected application's execution (

Web services are autonomous and heterogeneous computational entities. The need to build Web services rapidly has necessitated to realize ease of design and implementation through the paradigm of model based design, as a normal requirement rather than an exception. The specification, design and implementation of Web service applications need to address three major aspects: orchestration of services, conversation and choreography. In distributed computing, abstractions such as scripts have been used to abstract patterns of communication hiding low level details. In this paper, we demonstrate an approach of integrating orchestration with scripting to depict a pattern of communication or conversations among various agents. This leads to an effective specification language ScriptOrc for Web services choreography. We shall illustrate the usages with examples from workflow systems.

The performance of parallel programs can be largely affected by the latency of remote memory references. The notion of affinity has been used extensively for scheduling programmer defined threads to reduce remote communication costs. The most popular approach has been to schedule the thread as close to the data as possible. Most of the existing techniques expect the programmer to annotate affinity related information used by the scheduler. In this paper, we propose a framework that qualifies and quantifies various possible affinities playing a role in memory access latency in a system comprising of threads, processor nodes and data objects. We propose a technique based on cost functions to arrive at affinity information that can be used for reducing latencies. The affinity information thus obtained can be used in a number of ways such as: (1) transform the user program automatically (i.e., oblivious to the programmer); (2) highlight the user code in the integrated development toolkit used by the programmer; and (3) provide annotations that can be understood by the scheduler in making dynamic decisions of allocating objects and assigning threads to nodes. We support our framework and algorithm with the case studies/experiments done so far.

The specification, design and implementation of web service applications need to address three major aspects: Orchestration of Services, Conversation and Choreography. In distributed computing, abstractions such as scripts have been used to abstract patterns of communication hiding low level details. In this paper, we demonstrate an approach of integrating orchestration with scripting to depict a pattern of communication or conversations among various agents.

The efficient computation of exact abstractions of a concrete program for a given set of predicates is key to the efficiency of Counter-Example Guided Abstraction-Refinement (CEGAR). Recent work propose the use of DPLL-based SMT solvers, modified into enumerators. This technique has been successfully applied in the realm of software, where a control flow graph is available to direct the exploration. However this approach shows some limitations when the number of models grows: in fact, it intrinsically relies on the enumeration of all the implicants, which basically requires the enumerations of all the disjuncts in the DNF of the abstraction. In this paper, we propose a new technique to improve the construction of abstractions. We complement SMT solvers with the use of BDDs, which enables us to avoid the model explosion. Essentially, we exploit the fact that BDDs are a DAG representations of the space that a DPLL-based enumerator treats as a tree. A preliminary experimental evaluation shows the potential of the approach.

X10 is a modern object-oriented programming language designed for high performance, high productivity programming of parallel and multi-core computer systems. Compared to the lower-level thread-based concurrency model in the JavaTM language, X10 has higher-level concurrency constructs such as async, atomic and finish built into the language to simplify creation, analysis and optimization of parallel programs. In this paper, we introduce a new algorithm for May-Happen-in-Parallel (MHP) analysis of X10 programs. The analysis algorithm is based on simple path traversals in the Program Structure Tree, and does not rely on pointer alias analysis of thread objects as in MHP analysis for Java programs. We introduce a more precise definition of the MHP relation than in past work by adding condition vectors that identify execution instances for which the MHP relation holds, instead of just returning a single true/false value for all pairs of executing instances. Further, MHP analysis is refined in our approach by using the observation that two statement instances which occur in atomic sections that execute at the same X10 place must have MHP = false. We expect that our MHP analysis algorithm will be applicable to any language that adopts the core concepts of places, async, finish, and atomic sections from the X10 programming model. We also believe that this approach offers the best of two worlds to programmers and parallel programming tools ---higher-level abstractions of concurrency coupled with simple and efficient analysis algorithms.

In this paper,we address the problem of guaranteeing the absence of physical deadlock in the execution of a parallel program using the async, finish, atomic, and place constructs from the X10 language. First, we extend previous work-stealing memory bound results for fully strict multi-threaded computations to terminally strict multithreaded computations in which one activity may wait for completion of a descendant activity (as in X10's async and finish constructs), not just an immediate child (as in Cilk 's spawn and sync constructs). This result establishes physical dead-lock freedom for SMP deployments.Second,we introduce a new class of X10 deployments for clusters, which builds on an underlying Active Message network and the new concept of Doppelgänger mode execution of X10 activities. Third, we use this new class of deployments to establish physical deadlock freedom for deployments on clusters of uniprocessors.

SystemC is being widely used for system-level modeling of system-on-chip. When designing this class of system, one of the main challenges is to guarantee the correctness of the implementation. This can be especially difficult for designs that are composed of concurrent components with lot of interactions. Most designers use a component-based design approach, where one has an informal idea of how the design should behave, define component specifications, implement and assemble the components into a program, and then check for correctness by simulating the design with a number of testbenches. With this methodology, bugs often go undetected because when using simulation, it is very difficult to test for all possible interactions. To overcome this limitation, our goal is to establish a specification and verification methodology for SystemC. To address the scalability issue, which is a serious limiting factor in state-based verification approaches, we use the concepts of behavioral types; allowing us to effectively infer system properties from properties of its components. In this paper, we answer the following questions: (1) what is a behavioral type? (2) how are behavioral type defined? and (3) how to use the behavioral types in a compositional verification methodology

The Internet today is seeing the evolution of peer-to-peer (P2P) applications and interaction. Such interaction implies a direct communication between two end nodes of the Internet. P2P applications currently are facilitated by a central server, largely to ensure the authenticity of users. However; we foresee two issues with such a system - time/bandwidth usage for facilitation and non availability of a central facilitation server for P2P networks. We propose a security protocol called PGSP (peer group security protocol), relying on tamperproof hardware, to authenticate two peer nodes mutually. PGSP also establishes a secure channel between any two nodes without any central facilitation and, thus, allows for the two nodes to exchange a public-private key pair at the time of interaction. PGSP fits well with the resurrecting duckling security paradigm (Stajano, F. and Anderson, R., Proc. 3rd AT&T Software Symp., 1999). Once the hardware is imprinted for authentication, PGSP is robust against man-in-the-middle attack, passive eavesdropping and active impersonation attacks, ensuring source authentication, data confidentiality and data integrity. The proposed scheme is scalable to the addition of both new nodes and new P2P applications/groups to every node, and is cost-effective.

Verification of pipelined processors is a complex and challenging issue. In this paper, we develop a methodology based on translation validation for the verification of pipelined processors that support precise exceptions and out-of-order executions. We have developed a tool integrated with STeP theorem prover for the automatic verification of pipelined architectures. Formal verification of DLX processor is illustrated using our methodology. It is shown that the precise exception modelling is preserved over a range of pipeline instructions of DLX pipeline, like, integer, floating point, branch instructions, etc. The methodology is also illustrated with examples from DLX processor. A comparative evaluation of our method with other approaches is done and a structure of the tool is also provided.

Message Sequence Charts (MSCs) have gained wide acceptance for scenario-based specification of component behaviors. MSCs are very useful during requirements capture phase of the software development process and reveal errors in requirement specifications when used in early stages. As MSCs have found widespread usage, there have been several extensions to overcome its' shortcomings for a spectrum of applications keeping the rationale of MSCs invariant. In this paper, we propose (a) An extension of hierarchical MSCs (hMSC for short), called MSC/sup +/, keeping in view the need of complex reactive system specifications; it has new additional features such as watching (preemptive) construct, generalized coregions, and includes features for the specifications of live and forbidden scenarios. (b) A formal translation of MSC/sup +/, to the synchronous language ESTEREL is also provided, This feature enables validating requirement specifications and also to obtain a prototype for synchronous MSC/sup +/ specifications. Apart from obtaining a prototype, the translation of MSC/sup +/ to ESTEREL (that has clean and mathematical semantics) provides a clear semantic definition for the synchronous MSC/sup +/ specifications, In the paper, we describe, the design and implementation of MSC/sup +/ followed by the translation of MSC/sup +/, to ESTEREL leading to prototyping of systems. Examples are used to highlight characteristic features of the language, system and applications.

There is a growing demand for software tools that can assist in designing, analyzing and validating embedded real-time system applications. ESTEREL, a synchronous language, is widely used in the development of embedded systems and hardware/software codesign. We describe a method that uses timed annotations for ESTEREL programs that makes it possible to predict the timing constraints required to be satisfied by the embedded system. Using the specified annotations and the programming environment of ESTEREL, we describe a method and a tool for validating the concrete realization relative to time-annotated ESTEREL specifications. Also, the method derives time constraints to be satisfied by the concrete architectures for realizing the logical specification. We illustrate the technique with examples as well as the structure of the tool implemented.

In this paper, we discuss a new paradigm called Multiclock Esterel, based on the paradigm of the synchronous reactive language, Esterel, used for reactive systems and synchronous circuit design. We show that the Multiclock Esterel paradigm provides a general framework for the design of systems with multiple local clocks and the earlier paradigm of CRP (Communicating Reactive Processes) can be obtained as an instance of the newly proposed paradigm. Furthermore, it preserves the advantages of the classical Esterel paradigm and thus benefits from the advantages of verifiability of specifications/models. Multiclock Esterel provides a formal basis for designing asynchronous circuits and provides a succinct unification of synchrony and asynchrony.

We design a system with six Basic Combinators and prove that it is powerful enough to embed the full asynchronous π-calculus, including replication. Our theory for constructing Combinatory Versions of concurrent languages is based on a method, used by Quine and Bernays, for the general elimination of variables in linguistic formalisms. Our combinators are designed to eliminate the requirement of names that are bound by an input prefix . They also eliminate the need for input prefix, output prefix, and the accompanying mechanism of substitution . We define a notion of bisimulation for the combinatory version and show that the combinatory version preserves the semantics of the original calculus. One of the distinctive features of the approach is that it can be used to rework several process algebras in order to derive equivalent combinatory versions.

We describe a methodology for mapping linear recurrence equations to a spectrum of systolic architectures. First, we design a systolic program in a very general architecture referred to as Basic Systolic Architecture and establish the correctness of the implementation. Next, we show how efficient transformations/implementations of programs for different systolic architectures can be obtained through transformations such as projections and translations.

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...

A static analysis for reasoning about the temporal behaviors of programs in real-time distributed programming languages is proposed. The analysis is based on the action set semantics using the pure maximal parallelism model. It is shown how to specify and verify various timing properties of real-time programs. The approach provides only an approximate timing behavior, because the state information is ignored. However, many interesting properties such as parallel actions, deadlocks, livelocks, terminations, temporal errors, and failures, can be identified. Furthermore, the approach is compositional and thus makes it possible to reason about the timing properties incrementally. The method not only leads to efficient algorithms for the static analysis of CSP programs but also applies to many other languages.>

A description is given of language constructs for specifying concurrency in CDL*. The main goals in designing the language have been: modular specification, data integrity, and expressiveness. The language constructs are presented, and it is shown through examples how the constructs mirror the goals. The major advantages of the constructs are as follows: (1) data integrity is achieved without resorting to mutual exclusion unnecessarily, (2) dynamic resource management is achieved safely guaranteeing the anonymity of the dynamically allocating resources, and (3) similar components can be packaged together without resorting to sequential access. Various features of the language are illustrated through examples. In short, the language provides a step towards integrating abstraction mechanisms and specification techniques. Some of the features in CDL* are compared to some of the features available in other languages, including distributed programming languages.>