| 1. |
- Hojjat, Hossein, et al.
(författare)
-
Formal analysis of systemc designs in process algebra
- 2011
-
Ingår i: Fundamenta Informaticae. - Amsterdam : IOS Press. - 0169-2968 .- 1875-8681. ; 107, s. 19-42
-
Tidskriftsartikel (refereegranskat)abstract
- SystemC is an IEEE standard system-level language used in hardware/software co-design and has been widely adopted in the industry. This paper describes a formal approach to verifying SystemC designs by providing a mapping to the process algebra mCRL2. Our mapping formalizes both the simulation semantics as well as exhaustive state-space exploration of SystemC designs. By exploiting the existing reduction techniques of mCRL2 and also its model-checking tools, we efficiently locate the race conditions in a system and resolve them. A tool is implemented to automatically perform the proposed mapping. This mapping and the implemented tool enabled us to exploit process-algebraic verification techniques to analyze a number of case-studies, including the formal analysis of a single-cycle and a pipelined MIPS processor specified in SystemC.
|
|
| 2. |
- 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.
|
|
| 3. |
- Khakpour, Narges, et al.
(författare)
-
Assuring the Correctness of Large-scale Adaptive Systems
- 2011
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- The next generation of software systems includes systems composed of a large number of distributed, decentralized, autonomous, interacting, cooperating, organically grown, heterogeneous, and continually evolving subsystems, which we call IT Ecosystems. Clearly, we need novel models and approaches to design and develop such systems which can tackle the long-term evolution and complexity problems. In this paper, our framework to model IT-Ecosystems is a combination of top-down (centralized control) and bottom-up (self-organizing) approach. We use a flexible formal model, hierarchical PobSAM, that supports both behavioral and structural adaptation/evolution. We use a detailed, close to real-life, case study of a smart airport to show how we can use hierarchical PobSAM in modeling, analyzing and developing an IT Ecosystem. We provide an executable formal specification of the model in Maude, and use LTL model checking and bounded state space search provided by Maude to analyze the model. We develop a prototype of our case study designed by hierarchical PobSAM using Java and Ponder2. Due to the complexity of model, we can not check all properties at design time using Maude. We propose a new approach for run-time verification of our case study, and check different types of properties which we could not verify using model checking. As our model uses dynamic policies to control the behavior of system which can be modified at runtime, it provides us a suitable capability to react to the property violation by modification of policies.
|
|
| 4. |
- Khakpour, Narges, et al.
(författare)
-
Context-Based Behavioral Equivalence of Components in Self-Adaptive Systems
- 2011
-
Ingår i: Formal Methods and Software Engineering. 13th International Conference on Formal Engineering Methods (ICREM 2011). Durham, UK, 20111026. - Berlin, Heidelberg : Springer. ; , s. 16-32
-
Konferensbidrag (refereegranskat)abstract
- An important challenge to realize dynamic adaptation is finding suitable components for substitution or interaction according to the current context. A possible solution is checking behavioral equivalence of components in different contexts. Two components are equivalent with respect to a context, if they behave equivalently in that context. In this work, we deal with context-specific behavioral equivalence of PobSAM components. PobSAM is a flexible formal model for developing and modeling evolving self-adaptive systems. A PobSAM model is a collection of actors, views, and autonomous managers. Autonomous managers govern the behavior of actors by enforcing suitable context-based policies. Views provide contextual information for managers to control and adapt the actors behavior. Managers are the core components used to realize adaptation by changing their policies. They are modeled as meta-actors whose configurations are described using a multi-sorted algebra called CA. The behavior of mangers depends on the context in which they are executing. In this paper, we present an equational theory to reason about context-specific behavioral equivalence of managers independently from actors. To this end, we introduce and axiomatize a new operator to consider the interaction of managers and the context. This equational theory is based on the notion of statebased bisimilarity and allows us to reason about the behavioral equivalence of managers as well as the behavioral equivalence of the constitutes of managers (i.e., policies and configurations). We illustrate our approach through an example.
|
|
| 5. |
- Khakpour, Narges, et al.
(författare)
-
Formal analysis of policy-based self-adaptive systems
- 2010
-
Ingår i: Proceedings of the 2010 ACM Symposium on Applied Computing, SAC'10. - New York, NY, USA : ACM Press. - 9781605586397 ; , s. 2536-2543
-
Konferensbidrag (refereegranskat)abstract
- PobSAM is a flexible actor-based model with formal foundation for model-based development of self-adaptive systems. In PobSAM policies are used to control and adapt the system behavior, and allow us to decouple the adaptation concerns from the application code. In this paper, we use the actor-based language Rebeca to model check PobSAM models. Since policies are used to govern the system behavior, it is required to verify if the governing policies are enforced correctly. To this aim, we present a new generic classification of the policy conflicts and provide temporal patterns expressed in LTL to detect each class of conflicts. Moreover, we propose LTL patterns for checking the correctness of adaptation. An approach based on static analysis of adaptation policies is presented to check the system stability as well.
|
|
| 6. |
- 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.
|
|
| 7. |
- Khakpour, Narges, et al.
(författare)
-
HPobSAM for modeling and analyzing IT Ecosystems : Through a case study
- 2012
-
Ingår i: Journal of Systems and Software. - : Elsevier. - 0164-1212 .- 1873-1228. ; 85:12, s. 2770-2784
-
Tidskriftsartikel (refereegranskat)abstract
- The next generation of software systems includes systems composed of a large number of distributed, decentralized, autonomous, interacting, cooperating, organically grown, heterogeneous, and continually evolving subsystems, which we call IT Ecosystems. Clearly, we need novel models and approaches to design and develop such systems which can tackle the long-term evolution and complexity problems. In this paper, our framework to model IT Ecosystems is a combination of centralized control (top-down) and self-organizing (bottom-up) approach. We use a flexible formal model, HPobSAM, that supports both behavioral and structural adaptation/evolution. We use a detailed, close to real-life, case study of a smart airport to show how we can use HPobSAM in modeling, analyzing and developing an IT Ecosystem. We provide an executable formal specification of the model in Maude, and use LTL model checking and bounded state space search provided by Maude to analyze the model. We develop a prototype of our case study designed by HPobSAM using Java and Ponder2. Due to the complexity of the model, we cannot check all properties at design time using Maude. We propose a new approach for run-time verification of our case study, and check different types of properties which we could not verify using model checking. As our model uses dynamic policies to control the behavior of systems which can be modified at runtime, it provides us a suitable capability to react to the property violation by modification of policies.
|
|
