| 11. |
- 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.
|
|
| 12. |
- Aceto, Luca, et al.
(författare)
-
Rule Formats for Distributivity
- 2012
-
Ingår i: Theoretical Computer Science. - : Elsevier BV. - 0304-3975 .- 1879-2294. ; 458, s. 1-28
-
Tidskriftsartikel (refereegranskat)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. Some conditions ensuring the invalidity of the left-distributivity law are also offered. © 2012 Elsevier B.V. All rights reserved.
|
|
| 13. |
- Aceto, Luca, et al.
(författare)
-
Rule Formats for Distributivity
- 2011
-
Ingår i: Language and Automata Theory and Applications. - Heidelberg : Springer Berlin/Heidelberg. - 9783642212536 ; , s. 79-90
-
Konferensbidrag (refereegranskat)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. © 2011 Springer-Verlag.
|
|
| 14. |
- 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.
|
|
| 15. |
- Aceto, Luca, et al.
(författare)
-
SOS Rule Formats for Zero and Unit Elements
- 2011
-
Ingår i: Theoretical Computer Science. - Amsterdam : Elsevier. - 0304-3975 .- 1879-2294. ; 412:28, s. 3045-3071
-
Tidskriftsartikel (refereegranskat)abstract
- This paper proposes rule formats for Structural Operational Semantics guaranteeing that certain constants act as left or right unit/zero elements for a set of binary operators. Examples of left and right zero, as well as unit, elements from the literature are shown to fit the rule formats offered in this study. © 2011 Elsevier B.V. All rights reserved.
|
|
| 16. |
|
|
| 17. |
- 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.
|
|
| 18. |
- 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
|
|
| 19. |
- 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.
|
|
| 20. |
- 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.
|
|
