| 1. |
- Aceto, L., et al.
(författare)
-
Decompositional Reasoning about the History of Parallel Processes
- 2011
-
Ingår i: Fundamentals of software engineering. - Heidelberg : Springer Berlin/Heidelberg. - 1611-3349 .- 0302-9743. - 9783642293191 - 9783642293207 ; , s. 32-47
-
Konferensbidrag (refereegranskat)abstract
- This paper presents a decomposition technique for Hennessy-Milner logic with past and its extension with recursively defined formulae. In order to highlight the main ideas and technical tools, processes are described using a subset of CCS with parallel composition, nondeterministic choice, action prefixing and the inaction constant. The study focuses on developing decompositional reasoning techniques for parallel contexts in that language. © 2012 Springer-Verlag.
|
|
| 2. |
- Aceto, Luca, et al.
(författare)
-
Rule formats for determinism and idempotence
- 2012
-
Ingår i: Science of Computer Programming. - Amsterdam : Elsevier BV. - 0167-6423 .- 1872-7964. ; 77:7-8, s. 889-907
-
Tidskriftsartikel (refereegranskat)abstract
- Determinism is a semantic property of (a fragment of) a language that specifies that a program cannot evolve operationally in several different ways. Idempotence is a property of binary composition operators requiring that the composition of two identical specifications or programs will result in a piece of specification or program that is equivalent to the original components. In this paper, we propose (related) meta-theorems for guaranteeing the determinism and idempotence of binary operators. These meta-theorems are formulated in terms of syntactic templates for operational semantics, called rule formats. In order to obtain a powerful rule format for idempotence, we make use of the determinism of certain transition relations in the definition of the format for idempotence. We show the applicability of our formats by applying them to various operational semantics from the literature.
|
|
| 3. |
|
|
| 4. |
- Jaghoori, Mohammad Mahdi, et al.
(författare)
-
Symmetry and partial order reduction techniques in model checking Rebeca
- 2010
-
Ingår i: Acta Informatica. - New York : Springer. - 0001-5903 .- 1432-0525. ; 47:1, s. 33-66
-
Tidskriftsartikel (refereegranskat)abstract
- Rebeca is an actor-based language with formal semantics which is suitable for modeling concurrent and distributed systems and protocols. Due to its object model, partial order and symmetry detection and reduction techniques can be efficiently applied to dynamic Rebecamodels. We present two approaches for detecting symmetry in Rebeca models: One that detects symmetry in the topology of inter-connections among objects and another one which exploits specific data structures to reflect internal symmetry in the internal structure of an object. The former approach is novel in that it does not require any input from the modeler and can deal with the dynamic changes of topology. This approach is potentially applicable to a wide range of modeling languages for distributed and reactive systems. We have also developed a model checking tool that implements all of the above-mentioned techniques. The evaluation results show significant improvements in model size and model-checkingtime.
|
|
| 5. |
- Khakpour, Narges, et al.
(författare)
-
Formal modeling of evolving self-adaptive systems
- 2012
-
Ingår i: Science of Computer Programming. - Amsterdam : Elsevier. - 0167-6423 .- 1872-7964. ; 78:1, s. 3-26
-
Tidskriftsartikel (refereegranskat)abstract
- In this paper, we present a formal model, named PobSAM (Policy-based Self-Adaptive Model), for developing and modeling self-adaptive evolving systems. In this model, policies are used as a mechanism to direct and adapt the behavior of self-adaptive systems. A PobSAM model is a collection of autonomous managers and managed actors. The managed actors are dedicated to the functional behavior while the autonomous managers govern the behavior of managed actors by enforcing suitable policies. A manager has a set of configurations including two types of policies: governing policies and adaptation policies. To adapt the system behavior in response to the changes, the managers switch among different configurations. We employ the combination of an algebraic formalism and an actor-based model to specify this model formally. Managed actors are expressed by an actor model. Managers are modeled as meta-actors whose configurations are described using a multi-sorted algebra called CA. We provide an operational semantics for PobSAM using labeled transition systems. Furthermore, we provide behavioral equivalence of different sorts of CA in terms of splitting bisimulation and prioritized splitting bisimulation. Equivalent managers send the same set of messages to the actors. Using our behavioral equivalence theory, we can prove that the overall behavior of the system is preserved by substituting a manager by an equivalent one.
|
|
| 6. |
- Khakpour, Narges, et al.
(författare)
-
PobSAM : policy-based managing of actors in self-adaptive systems
- 2010
-
Ingår i: Proceedings of the 6th International Workshop on Formal Aspects of Component Software (FACS’09, Eindhoven, The Netherlands, November 2-3, 2009). - Amsterdam : Elsevier. ; 263, s. 129-143
-
Konferensbidrag (refereegranskat)
|
|
| 7. |
- Aceto, Luca, et al.
(författare)
-
A rule format for unit elements
- 2010
-
Ingår i: SOFSEM 2010. - Berlin : Springer Berlin/Heidelberg. - 9783642112652 - 9783642112669 ; , s. 141-152
-
Konferensbidrag (refereegranskat)abstract
- This paper offers a meta-theorem for languages with a Structural Operational Semantics (SOS) in the style of Plotkin. Namely, it proposes a generic rule format for SOS guaranteeing that certain constants act as left- or right-unit elements for a set of binary operators. We show the generality of our format by applying it to a wide range of operators from the literature on process calculi.
|
|
| 8. |
- Aceto, Luca, et al.
(författare)
-
Decompositional Reasoning about the History of Parallel Processes
- 2010
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Decompositional reasoning aims at automatically decomposing a global property of a composite system into local properties of (possibly unknown) components. In concurrency theory, decompositional reasoning techniques date back to the seminal work of Larsen and Liu in the late 1980s and early 1990s. However, we are not aware of any such decomposition technique that applies to reasoning about the "past". In this paper, we address this problem and present a decomposition technique for Hennessy-Milner logic with past and its extension with recursively defined formulae. As a language for processes, we use a subset of Milner's CCS with parallel composition, non-deterministic choice, action prefixing and the inaction constant. We focus on developing decompositional reasoning techniques for parallel contexts in that language.
|
|
| 9. |
- Aceto, Luca, et al.
(författare)
-
Exploiting Algebraic Laws to Improve Mechanized Axiomatizations
- 2013
-
Ingår i: Algebra and Coalgebra in Computer Science. - Berlin : Springer Berlin/Heidelberg. - 9783642402067 - 9783642402050 ; , s. 36-50
-
Konferensbidrag (refereegranskat)abstract
- In the field of structural operational semantics (SOS), there have been several proposals both for syntactic rule formats guaranteeing the validity of algebraic laws, and for algorithms for automatically generating ground-complete axiomatizations. However, there has been no synergy between these two types of results. This paper takes the first steps in marrying these two areas of research in the meta-theory of SOS and shows that taking algebraic laws into account in the mechanical generation of axiomatizations results in simpler axiomatizations. The proposed theory is applied to a paradigmatic example from the literature, showing that, in this case, the generated axiomatization coincides with a classic hand-crafted one. © 2013 Springer-Verlag Berlin Heidelberg.
|
|
| 10. |
- Aceto, L., et al.
(författare)
-
Lifting non-finite axiomatizability results to extensions of process algebras
- 2010
-
Ingår i: Acta Informatica. - Amsterdam : Elsevier. - 0001-5903 .- 1432-0525. ; 47:3, s. 147-177
-
Tidskriftsartikel (refereegranskat)abstract
- This paper presents a general technique for obtaining new results pertaining to the non-finite axiomatizability of behavioural (pre)congruences over process algebras from old ones. The proposed technique is based on a variation on the classic idea of reduction mappings. In this setting, such reductions are translations between languages that preserve sound (in)equations and (in)equational provability over the source language, and reflect families of (in)equations responsible for the non-finite axiomatizability of the target language. The proposed technique is applied to obtain a number of new non-finite axiomatizability theorems in process algebra via reduction to Moller's celebrated non-finite axiomatizability result for CCS. The limitations of the reduction technique are also studied. In particular, it is shown that prebisimilarity is not finitely based over CCS with the divergent process Ω, but that this result cannot be proved by a reduction to the non-finite axiomatizability of CCS modulo bisimilarity. This negative result is the inspiration for the development of a sharpened reduction method that is powerful enough to show that prebisimilarity is not finitely based over CCS with the divergent process Ω. © 2010 Springer-Verlag.
|
|
