| 1. |
- Khamespanah, Ehsan, et al.
(författare)
-
State Distribution Policy for Distributed Model Checking of Actor Models
- 2015
-
Ingår i: Electronic Communications of the EASST. - Berlin : Universitätsverlag der TU Berlin. - 1863-2122. ; 72, s. 1-15
-
Tidskriftsartikel (refereegranskat)abstract
- Model checking temporal properties is often reduced to finding accepting cycles in Büchi automata. A key ingredient for an effective distributed model checking technique is a distribution policy that does not split the potential accepting cycles of the corresponding automaton among several nodes. In this paper, we introduce a distribution policy to reduce the number of split cycles. This policy is based on the call dependency graph, obtained from the message passing skeleton of the model. We prove theoretical results about the correspondence between the cycles of call dependency graph and the cycles of the concrete state space and provide empirical data obtained from applying our distribution policy in state space generation and reachability analysis. We take Rebeca, an imperative interpretation of actors, as our modeling language and implement the introduced policy in its distributed state space generator. Our technique can be applied to other message-driven actor-based models where concurrent objects or services are units of concurrency.
|
|
| 2. |
|
|
| 3. |
- Hafemann Fragal, Vanderson, 1988-
(författare)
-
Automatic generation of configurable test-suites for software product lines
- 2018
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Software Product Line Engineering (SPLE) is an approach used in the development of similar products, which aims at systematic reuse of software artifacts. The SPLE process has several activities executed to assure software quality. Quality assurance is of vital importance for achieving and maintaining a high quality for various artifacts, such as products and processes. Testing activities are widely used in industry for quality assurance. However, the effort for applying testing is usually high, and increasing the testing efficiency is a major concern. A common means of increasing efficiency is automation of test design. Several techniques, processes, and strategies were developed for SPLE testing, but still many problems are open in this area of research. The challenge in focus is the reduction of the overall test effort required to test SPLE products. Test effort can be reduced by maximizing test reuse using models that take advantage of the similarity between products. The thesis goal is to automate the generation of small test-suites with high fault detection and low test redundancy between products. To achieve the goal, equivalent tests are identified for a set of products using complete and configurable test-suites. Two research directions are explored, one is product-based centered, and the other is product line-centered. For test design, test-suites that have full fault coverage were generated from state machines with and without feature constraints. A prototype tool was implemented for test design automation. In addition, the proposed approach was evaluated using examples, experimental studies, and an industrial case study for the automotive domain. The results of the product-based centered approach indicate a reduction of 36% on the number of test cases that need to be concretized. The results of the product line-centered approach indicate a reduction of 50% on the number of test cases generated for groups of product configurations.
|
|
| 4. |
- Araujo, Hugo, et al.
(författare)
-
Sound conformance testing for cyber-physical systems : Theory and implementation
- 2018
-
Ingår i: Science of Computer Programming. - Amsterdam : ELSEVIER SCIENCE BV. - 0167-6423 .- 1872-7964. ; 162, s. 35-54
-
Tidskriftsartikel (refereegranskat)abstract
- Conformance testing is a formal and structured approach to verifying system correctness. We propose a conformance testing algorithm for cyber-physical systems, based on the notion of hybrid conformance by Abbas and Fainekos. We show how the dynamics of system specification and the sampling rate play an essential role in making sound verdicts. We specify and prove error bounds that lead to sound test-suites for a given specification and a given sampling rate. We use reachability analysis to find such bounds and implement the proposed approach using the CORA toolbox in Matlab. We apply the implemented approach on a case study from the automotive domain.
|
|
| 5. |
- Aceto, Luca, et al.
(författare)
-
A Rule Format for Unit Elements
- 2009
-
Rapport (övrigt vetenskapligt/konstnärligt)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.
|
|
| 6. |
- 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.
|
|
| 7. |
- 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.
|
|
| 8. |
- 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.
|
|
| 9. |
- 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.
|
|
| 10. |
- Aerts, Arend, et al.
(författare)
-
A Tool Prototype for Model-Based Testing of Cyber-Physical Systems
- 2015
-
Ingår i: Theoretical Aspects of Computing – ICTAC 2015. - Cham : Springer. - 9783319251493 - 9783319251509 ; , s. 563-572
-
Konferensbidrag (refereegranskat)abstract
- We report on a tool prototype for model-based testing of cyber-physical systems. Our starting point is a hybrid-system model specified in a domain-specific language called Acumen. Our prototype tool is implemented in Matlab and covers three stages of model-based testing, namely, test-case generation, test-case execution, and conformance analysis. We have applied our implementation to a number of typical examples of cyber-physical systems in order to analyze its applicability. In this paper, we report on the result of applying the prototype tool on a DC-DC boost converter. © Springer International Publishing Switzerland 2015
|
|
