| 1. |
- 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.
|
|
| 2. |
- 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.
|
|
| 3. |
- Aceto, Luca, et al.
(författare)
-
On Rule Formats for Zero and Unit Elements
- 2010
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- This paper proposes a rule format for Structural Operational Semantics guaranteeing that certain constants act as left or right zero elements for a set of binary operators. Our design approach is also applied to reformulate an earlier rule format for unit elements developed by some of the authors. Examples of left and right zero, as well as unit, elements from the literature are shown to be checkable using the provided formats.
|
|
| 4. |
- Aceto, Luca, et al.
(författare)
-
Rule Formats for Distributivity
- 2010
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- This paper proposes rule formats for Structural Operational Semantics guaranteeing that certain binary operators are left distributive with respect to a set of binary operators. Examples of left-distributivity laws from the literature are shown to be instances of the provided formats.
|
|
| 5. |
- Atif, Muhammad, et al.
(författare)
-
Reconstruction and verification of group membership protocols
- 2010
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- In this paper, we present a process-algebraic specication of group membership protocols specified in [Y. Amir, D. Dolev, S. Kramer and D. Malki, Membership Algorithms for Multicast Communication Groups, Springer-Verlag, 1992]. In order to formalise the protocol and its properties we disambiguate the informal specification provided by the paper. This requires trying different possible interpretations in the formal model and checking the consistency of the assumption and formally verifying the correctness properties. We thus present a formal reconstruction of the membership algorithms and model-check our reconstruction.
|
|
| 6. |
- Beohar, Harsh, 1984-, et al.
(författare)
-
Input-output conformance testing based on featured transition systems
- 2014
-
Ingår i: Proceedings of the 29th Annual ACM Symposium on Applied Computing. - New York, NY, USA : Association for Computing Machinery (ACM). - 9781450324694 ; , s. 1272-1278
-
Konferensbidrag (refereegranskat)abstract
- We extend the theory of input-output conformance testing to the setting of software product lines. In particular, we allow for input-output featured transition systems to be used as the basis for generating test suites and test cases. We introduce refinement operators both at the level of models and at the level of test suites that allow for projecting them into a specific product configuration (or a product sub-line). We show that the two sorts of refinement are consistent and lead to the same set of test-cases. © Copyright 2014 ACM
|
|
| 7. |
- Beohar, Harsh, 1984-, et al.
(författare)
-
Spinal test suites for software product lines
- 2014
-
Ingår i: Proceedings. - Sydney : Open Publishing Association. ; , s. 44-55
-
Konferensbidrag (refereegranskat)abstract
- A major challenge in testing software product lines is efficiency. In particular, testing a product line should take less effort than testing each and every product individually. We address this issue in the context of input-output conformance testing, which is a formal theory of model-based testing. We extend the notion of conformance testing on input-output featured transition systems with the novel concept of spinal test suites. We show how this concept dispenses with retesting the common behavior among different, but similar, products of a software product line. © H. Beohar & M.R. Mousavi.
|
|
| 8. |
- Churchill, Martin, et al.
(författare)
-
Modular Semantics for Transition System Specifications with Negative Premises
- 2013
-
Ingår i: Proceedings of the 24th International Conference on Concurrency Theory. - Heidelberg : Springer Berlin/Heidelberg. - 9783642401831 - 9783642401848 ; , s. 46-60
-
Konferensbidrag (refereegranskat)abstract
- Transition rules with negative premises are needed in the structural operational semantics of programming and specification constructs such as priority and interrupt, as well as in timed extensions of specification languages. The well-known proof-theoretic semantics for transition system specifications involving such rules is based on well-supported proofs for closed transitions. Dealing with open formulae by considering all closed instances is inherently non-modular - proofs are not necessarily preserved by disjoint extensions of the transition system specification. Here, we conservatively extend the notion of well-supported proof to open transition rules. We prove that the resulting semantics is modular, consistent, and closed under instantiation. Our results provide the foundations for modular notions of bisimulation such that equivalence can be proved with reference only to the relevant rules, without appealing to all existing closed instantiations of terms. © 2013 Springer-Verlag.
|
|
| 9. |
- Cimini, Matteo, et al.
(författare)
-
Nominal SOS
- 2012
-
Ingår i: Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII). - Amsterdam : Elsevier. ; , s. 103-116
-
Konferensbidrag (refereegranskat)abstract
- Plotkin’s style of Structural Operational Semantics (SOS) has become a de facto standard in giving operational semantics to formalisms and process calculi. In many such formalisms and calculi, the concepts of names, variables and binders are essential ingredients. In this paper, we propose a formal framework for dealing with names in SOS. The framework is based on the Nominal Logic of Gabbay and Pitts and hence is called Nominal SOS. We define nominal bisimilarity, an adaptation of the notion of bisimilarity that is aware of binding. We provide evidence of the expressiveness of the framework by formulating the early π-calculus and Abramsky’s lazy λ-calculus within Nominal SOS. For both calculi we establish the operational correspondence with the original calculi. Moreover, in the context of the π-calculus, we prove that nominal bisimilarity coincides with Sangiorgi’s open bisimilarity and in the context of the λ-calculus we prove that nominal bisimilarity coincides with Abramsky’s applicative bisimilarity. © 2012 Elsevier B.V.
|
|
| 10. |
- Dechesne, Francien, et al.
(författare)
-
Interpreted Systems Semantics for Process Algebra with Identity Annotations
- 2013
-
Ingår i: Logic, Language, and Computation. - Heidelberg : Springer Berlin/Heidelberg. - 9783642369759 - 9783642369766 ; , s. 182-205
-
Bokkapitel (refereegranskat)abstract
- Process algebras have been developed as formalisms for specifying the behavioral aspects of protocols. Interpreted systems have been proposed as a semantic model for multi-agent communication. In this paper, we connect these two formalisms by defining an interpreted systems semantics for a generic process algebraic formalism. This allows us to translate and compare the vast body of knowledge and results for each of the two formalisms to the other and perform epistemic reasoning, e.g., using model-checking tools for interpreted systems, on process algebraic specifications. Based on our translation we formulate and prove some results about the interpreted systems generated by process algebraic specifications. © 2013 Springer-Verlag.
|
|
