| 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. |
- 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
|
|
| 3. |
- Arts, Thomas, et al.
(författare)
-
Automatic Consequence Analysis of Automotive Standards (AUTO-CAAS) [Position Paper]
- 2015
-
Ingår i: WASA '15. - New York, NY : ACM Press. - 9781450334440 ; , s. 35-38
-
Konferensbidrag (refereegranskat)abstract
- This paper provides some background and the roadmap of the AUTO-CAAS project, which is a 3-year project financed by the Swedish Knowledge Foundation and is ongoing as a joint project among three academic and industrial partners. The aim of the project is to exploit the formal models of the AUTOSAR standard, developed by the industrial partner of the project Quviq AB, in order to predict possible future failures in concrete implementations of components. To this end, the deviations from the formal specification will be exploited to generate test-cases that can push concrete components to the corners where such deviation will result in observable failures. The same information will also be used in the diagnosis of otherwise detected failures in order to pinpoint their root causes.
|
|
| 4. |
- Beohar, Harsh, 1984-, et al.
(författare)
-
A Pre-congruence Format for XY-simulation
- 2015
-
Ingår i: Fundamentals of Software Engineering. - Cham : Springer. - 9783319246437 - 9783319246444 ; , s. 215-229
-
Konferensbidrag (refereegranskat)abstract
- XY-simulation is a generalization of bisimulation that is parameterized with two subsets of actions. XY-simulation is known in the literature under different names such as modal refinement, partial bisimulation, and alternating simulation. In this paper, we propose a precongruence rule format for XY-simulation. The format allows for checking compositionality of XY-simulation for an arbitrary language with structural operational semantics, by performing very simple checks on the syntactic shape of the rules. We apply our format to derive concrete compositionality results for different notions of behavioral pre-order with respect to different process calculi in the literature. © IFIP International Federation for Information Processing 2015
|
|
| 5. |
|
|
| 6. |
- Khakpour, Narges, et al.
(författare)
-
Notions of Conformance Testing for Cyber-Physical Systems : Overview and Roadmap
- 2015
-
Ingår i: 26th International Conference on Concurrency Theory. - Wadern : Dagstuhl Publishing. - 9783939897910 ; , s. 18-40
-
Konferensbidrag (populärvet., debatt m.m.)abstract
- We review and compare three notions of conformance testing for cyber-physical systems. We begin with a review of their underlying semantic models and present conformance-preserving translations between them. We identify the differences in the underlying semantic models and the various design decisions that lead to these substantially different notions of conformance testing. Learning from this exercise, we reflect upon the challenges in designing an “ideal” notion of conformance for cyber-physical systems and sketch a roadmap of future research in this domain.
|
|
| 7. |
- Mousavi, Mohammad Reza, 1978-, et al.
(författare)
-
Timed-Gamma and Its Coordination Language
- 2015
-
Ingår i: Nordic Journal of Computing. - Helsinki : University of Helsinki. - 1236-6064. ; 15:2, s. 75-111
-
Tidskriftsartikel (refereegranskat)abstract
- This paper proposes a theoretical framework for separation of concerns in the formal specification of reactive and real-time systems. This framework consists of the syntax and the semantics of three languages (and all meaningful combinations thereof) that each address a separate concern. The first language, Gamma (a variant of an existing language) is used to define the functionality of a system (by means of a set of basic data transformations). Our additions are a simple language of intervals specifying timing-properties of basic transformations and a language (called Schedules) for specifying the coordination of the basic Gamma transformations. Each of these languages formally models a separate aspect of a system and statements in these languages can be reused, changed or analyzed in their own right. Our key contribution is that we provide a formal framework in which different combinations of aspects have a well-defined semantics.
|
|
| 8. |
- Noroozi, Neda, et al.
(författare)
-
Synchrony and asynchrony in conformance testing
- 2015
-
Ingår i: Software and Systems Modeling. - Heidelberg : Springer. - 1619-1366 .- 1619-1374. ; 14:1, s. 149-172
-
Tidskriftsartikel (refereegranskat)abstract
- We present and compare different notions of conformance testing based on labeled transition systems. We formulate and prove several theorems which enable using synchronous conformance testing techniques such as input–output conformance testing (ioco) in order to test implementations only accessible through asynchronous communication channels. These theorems define when the synchronous test cases are sufficient for checking all aspects of conformance that are observable by asynchronous interaction with the implementation under test. © 2015, Springer-Verlag Berlin Heidelberg.
|
|
| 9. |
- Varshosaz, Mahsa, 1985-, et al.
(författare)
-
Delta-Oriented FSM-Based Testing
- 2015
-
Ingår i: Formal Methods and Software Engineering. - Cham : Springer. - 9783319254227 - 9783319254234 ; , s. 366-381
-
Konferensbidrag (refereegranskat)abstract
- We use the concept of delta-oriented programming to organize FSM-based test models in an incremental structure. We then exploit incremental FSM-based testing to make efficient use of this high-level structure in generating test cases. We show how our approach can lead to more efficient test-case generation, both by analyzing the complexity of the test-case generation algorithm and by applying the technique to a case study. © Springer International Publishing Switzerland 2015
|
|
