The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
We show how declarative diagnosis techniques can be extended to cope with verification of operational properties, such as computed answers, and of abstract properties, such as types and groundness dependencies. The extension is achieved by using a simple semantic framework, based on abstract interpretation. The resulting technique (abstract diagnosis) leads to elegant bottom-up and top-down verification...
We are concerned with the static analysis of the communication topology for systems of mobile processes. For this purpose we construct an abstract interpretation of a large fragment of the π-calculus which can be used as a metalanguage to specify the behaviour of these systems. The abstract domain is expressive enough to give accurate descriptions of infinite and non-uniform distributions of processes...
The techniques of classical abstract interpretation are extended to the big- and small-step operational semantics of higher-order and communicative languages: Well-known techniques, such as memoization, and lesser-known ones, such as abstraction on program syntax, are employed to generate finite abstract interpretations of source programs based on their formal operational semantic definitions. The...
Mobile agents are code-containing objects that may be transmitted between communicating participants in a distributed system. Compared to systems that only allow the exchange of nonexecutable data, those incorporating mobile agents can achieve significant gains in performance and functionality. Languages with first-class functions provide a good starting point for agent programming, as they...
This document aims to provide a formal semantics for an object-oriented language with constructs for concurrency and distribution. The semantics is defined via a translation into the π-calculus process algebra. As is (perhaps regrettably) standard when giving the semantics of a language in such a way, we concentrate on faithfully capturing the program dynamics while abstracting away from many important...
We enhance Gamma, a multiset rewriting language, with a notion of structured multiset. A structured multiset is a set of addresses satisfying specific relations which can be used in the rewriting rules of the program. A type is defined by a context-free graph grammar and a structured multiset belongs to a type T if its underlying set of addresses satisfies the invariant expressed by the grammar defining...
The integration of polymorphism (in the style of the ML let-construct), subtyping, and effects (modelling assignment or communication) into one common type system has proved remarkably difficult. One line of research has succeeded in integrating polymorphism and subtyping; adding effects in a straightforward way results in a semantically unsound system. Another line of research has succeeded in integrating...
We study an annotated type and effect system that integrates let-polymorphism, effects, and subtyping into an annotated type and effect system for a fragment of Concurrent ML. First a small-step operational semantics is defined and next the annotated type and effect system is proved semantically sound. This provides insights into the rule for generalisation in the annotated type and effect system.
We study an annotated type and effect system that integrates let-polymorphism, effects, and subtyping into an annotated type and effect system for a fragment of Concurrent ML. First we define a type inference algorithm and then construct procedures for constraint normalisation and simplification. Next these algorithms are proved syntactically sound with respect to the annotated type and effect system.
The aim of the paper is to share the design problems we experienced when we were implementing a prototype analyzer of an asynchronous concurrent language. This new kind of static analyzer is based on previous work about operational semantics of parallel languages that can express concurrency and non-determinism of actions: it constructs abstract automata reflecting all the possible execution behaviours...
Flow analysis is a potentially very useful analysis for higher order functional languages, but its practical application has been slow in coining, partially hindered by shortcomings of the current analysis techniques. Among these are the limited precision, long analysis times, incompatibility with separate compilation, inapplicability to untyped languages and sensitivity to program structure associated...
Great hopes in the exploitation of the (implicit) parallelism inherent in functional programs have driven a number of projects. General frustration resulted wherever implementations on distributed memory machines were attempted. The grain size of potentially parallel tasks is too small to amortize the enormous costs of the necessary communication. The management of the parallelism is expensive. Decision...
We propose a structural operational semantics that expresses temporal aspects of mobile and distributed systems, each sequential component of which has its local clock. Since the run-time support of a programming language implements the operations of the language via some lower-level routines, the same action, put in different contexts, may have different durations. Also the network topology affects...
The algebraic approach to concurrency is tuned for modelling operational semantics and supporting formal verification of distributed imperative programs with asynchronous communications. We consider an imperative process algebra, IPAL, which is obtained by embedding the Linda primitives for interprocess communication in a CSP-like process description language enriched with a construct for assignment...
Mobile agents, i.e. pieces of programs that can be sent around networks of computers, are starting to appear on the Internet. Such programs may be seen as an enrichment of traditional distributed computing. Since mobile agents may carry communication links with them as they move across the network, they create very dynamic interconnection structures that can be extremely complex to analyse. In this...
In recent years many techniques have been developed for automatically verifying concurrent systems and most of them are based on a representation of the concurrent system by means of a finite state transition system. State explosion is one of the most serious problems of this approach: in fact often the prohibitive number of states renders the verification inefficient and, in some cases, impossible...
We define a compositional labelled transition system semantics for statecharts via a translation into a new process language called SP. The main novelty of the language is an operator of process refinement, which reflects the statecharts hierarchical structure. The translation agrees with Pnueli and Shalev semantics of statecharts. However, since the language is parametric in the set of basic actions...
The paper examines the specification language Statecharts from the point of view of its capability to express notions of priority. First a version of Statecharts that does not support priority is introduced, then various syntactic and semantics extensions are examined and compared from the point of view of expressing a general notion of priority. Finally, a special kind of priority, interrupt, is...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.