lnu.sePublications
Change search
Link to record
Permanent link

Direct link
BETA
Publications (10 of 21) Show all publications
Bagheri, M., Sirjani, M., Khamespanah, E., Khakpour, N., Akkaya, I., Movaghar, A. & Lee, E. A. (2018). Coordinated actor model of self-adaptive track-based traffic control systems. Journal of Systems and Software, 143, 116-139
Open this publication in new window or tab >>Coordinated actor model of self-adaptive track-based traffic control systems
Show others...
2018 (English)In: Journal of Systems and Software, ISSN 0164-1212, E-ISSN 1873-1228, Vol. 143, p. 116-139Article in journal (Refereed) Published
Abstract [en]

Self-adaptation is a well-known technique to handle growing complexities of software systems, where a system autonomously adapts itself in response to changes in a dynamic and unpredictable environment. With the increasing need for developing self-adaptive systems, providing a model and an implementation platform to facilitate integration of adaptation mechanisms into the systems and assuring their safety and quality is crucial. In this paper, we target Track-based Traffic Control Systems (TTCSs) in which the traffic flows through pre-specified sub-tracks and is coordinated by a traffic controller. We introduce a coordinated actor model to design self-adaptive TTCSs and provide a general mapping between various TTCSs and the coordinated actor model. The coordinated actor model is extended to build large-scale self-adaptive TTCSs in a decentralized setting. We also discuss the benefits of using Ptolemy II as a framework for model-based development of large-scale self-adaptive systems that supports designing multiple hierarchical MAPE-K feedback loops interacting with each other. We propose a template based on the coordinated actor model to design a self-adaptive TTCS in Ptolemy II that can be instantiated for various TTCSs. We enhance the proposed template with a predictive adaptation feature. We illustrate applicability of the coordinated actor model and consequently the proposed template by designing two real-life case studies in the domains of air traffic control systems and railway traffic control systems in Ptolemy II.

Place, publisher, year, edition, pages
Elsevier, 2018
Keywords
Self-adaptive systems, Track-based traffic control systems, Model@Runtime, MAPE-K feedback loop, Ptolemy II framework
National Category
Computer and Information Sciences
Research subject
Computer and Information Sciences Computer Science, Computer Science
Identifiers
urn:nbn:se:lnu:diva-77374 (URN)10.1016/j.jss.2018.05.034 (DOI)000438180000009 ()
Available from: 2018-08-30 Created: 2018-08-30 Last updated: 2018-08-30Bibliographically approved
Bagheri, M., Akkaya, I., Khamespanah, E., Khakpour, N., Sirjani, M., Movaghar, A. & Lee, E. A. (2017). Coordinated actors for reliable self-adaptive systems. In: FACS 2016 : Formal Aspects of Component Software: International Workshop on Formal Aspects of Component Software. Paper presented at 13th International Conference on Formal Aspects of Component Software, FACS 2016; Besancon; France; 19 - 21 October, 2016 (pp. 241-259). Springer
Open this publication in new window or tab >>Coordinated actors for reliable self-adaptive systems
Show others...
2017 (English)In: FACS 2016 : Formal Aspects of Component Software: International Workshop on Formal Aspects of Component Software, Springer, 2017, p. 241-259Conference paper, Published paper (Refereed)
Abstract [en]

Self-adaptive systems are systems that automatically adapt in response to environmental and internal changes, such as possible failures and variations in resource availability. Such systems are often realized by a MAPE-K feedback loop, where Monitor, Analyze, Plan and Execute components have access to a runtime model of the system and environment which is kept in the Knowledge component. In order to provide guarantees on the correctness of a self-adaptive system at runtime, the MAPE-K feedback loop needs to be extended with assurance techniques. To address this issue, we propose a coordinated actor-based approach to build a reusable and scalable model@runtime for self-adaptive systems in the domain of track-based traffic control systems. We demonstrate the approach by implementing an automated Air Traffic Control system (ATC) using Ptolemy tool.We compare different adaptation policies on the ATC model based on performance metrics and analyze combination of policies in different configurations of the model. We enriched our framework with runtime performance analysis such that for any unexpected change, subsequent behavior of the model is predicted and results are used for adaptation at the change-point. Moreover, the developed framework enables checking safety properties at runtime. © Springer International Publishing AG 2017.

Place, publisher, year, edition, pages
Springer, 2017
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 10231
Keywords
Air Traffic Control System, Cyber physical system, Model@runtime, Performance analysis, Self-adaptive system
National Category
Software Engineering
Research subject
Computer Science, Software Technology
Identifiers
urn:nbn:se:lnu:diva-64659 (URN)10.1007/978-3-319-57666-4_15 (DOI)000418342500015 ()2-s2.0-85018304749 (Scopus ID)978-3-319-57665-7 (ISBN)978-3-319-57666-4 (ISBN)
Conference
13th International Conference on Formal Aspects of Component Software, FACS 2016; Besancon; France; 19 - 21 October, 2016
Available from: 2017-06-02 Created: 2017-06-02 Last updated: 2018-01-13Bibliographically approved
Khakpour, N., Arbab, F. & Rutten, E. (2016). Synthesizing structural and behavioral control for reconfigurations in component-based systems. Formal Aspects of Computing, 28(1), 21-43
Open this publication in new window or tab >>Synthesizing structural and behavioral control for reconfigurations in component-based systems
2016 (English)In: Formal Aspects of Computing, ISSN 0934-5043, E-ISSN 1433-299X, Vol. 28, no 1, p. 21-43Article in journal (Refereed) Published
Abstract [en]

Correctness of the behavior of an adaptive system during dynamic adaptation is an important challenge to realize correct adaptive systems. Dynamic adaptation refers to changes to both the functionality of the computational entities that comprise a composite system, as well as the structure of their interconnections, in response to variations in the environment, e.g., the load of requests on a server system. In this research, we view the problem of correct structural adaptation as a supervisory control problem and synthesize a reconfiguration controller that guides the behavior of a system during adaptation. The reconfiguration controller observes the system behavior during an adaptation and controls the system behavior by allowing/disallowing actions in a way to ensure that a given property is satisfied and a deadlock is avoided. The system during adaptation is modeled using a graph transition system and properties to be enforced are specified using a graph automaton. We adapt a classical theory of supervisory control for synthesizing a controller for controlling the behavior of a system modeled using graph transition systems. This theory is used to synthesize a controller that can impose both behavioral and structural constraints on the system during an adaptation. We apply a tool that we have implemented to support our approach on a case study involving https servers.

National Category
Computer Systems
Research subject
Computer and Information Sciences Computer Science, Computer Science
Identifiers
urn:nbn:se:lnu:diva-51014 (URN)10.1007/s00165-015-0346-y (DOI)000372262000002 ()2-s2.0-84961155481 (Scopus ID)
External cooperation:
Available from: 2016-03-18 Created: 2016-03-18 Last updated: 2017-11-30Bibliographically approved
Khakpour, N. & Mousavi, M. R. (2015). Notions of Conformance Testing for Cyber-Physical Systems: Overview and Roadmap. In: Luca Aceto, David de Frutos Escrig (Ed.), 26th International Conference on Concurrency Theory (CONCUR 2015): . Paper presented at 26th International Conference on Concurrency Theory, CONCUR 2015, 1 September 2015 through 4 September 2015 (pp. 18-40). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Open this publication in new window or tab >>Notions of Conformance Testing for Cyber-Physical Systems: Overview and Roadmap
2015 (English)In: 26th International Conference on Concurrency Theory (CONCUR 2015) / [ed] Luca Aceto, David de Frutos Escrig, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik , 2015, p. 18-40Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2015
Series
Leibniz International Proceedings in Informatics (LIPIcs), ISSN 1868-8969 ; 42
Keywords
Cyber-physical systems, hybrid systems, conformance testing, model-based testing, behavioral pre-orders, hybrid input-output conformance testing
National Category
Computer Systems
Research subject
Computer and Information Sciences Computer Science, Computer Science
Identifiers
urn:nbn:se:lnu:diva-51015 (URN)10.4230/LIPIcs.CONCUR.2015.18 (DOI)2-s2.0-84958233342 (Scopus ID)978-3-939897-91-0 (ISBN)
Conference
26th International Conference on Concurrency Theory, CONCUR 2015, 1 September 2015 through 4 September 2015
Available from: 2016-03-18 Created: 2016-03-18 Last updated: 2016-08-09Bibliographically approved
Khakpour, N., Arbab, F. & Rutten, E. (2014). Supervisory Controller Synthesis for Safe Software Adaptation. In: Jean-Jacques Lesage, Jean-Marc Faure, Jose E. R. Cury, Bengt Lennartson (Ed.), 12th IFAC International Workshop on Discrete Event Systems (2014): . Paper presented at 12th International Workshop on Discrete Event Systems (2014), Cachan, France, 14-15 May, 2014 (pp. 39-45). International Federation of Automatic Control, 47, Iss 2
Open this publication in new window or tab >>Supervisory Controller Synthesis for Safe Software Adaptation
2014 (English)In: 12th IFAC International Workshop on Discrete Event Systems (2014) / [ed] Jean-Jacques Lesage, Jean-Marc Faure, Jose E. R. Cury, Bengt Lennartson, International Federation of Automatic Control , 2014, Vol. 47, Iss 2, p. 39-45Conference paper, Published paper (Refereed)
Abstract [en]

Today's software systems need to adapt their behavior due to the changes in their operational environments and user requirements. To this end, an adaptive software performs a sequence of adaptations at runtime. Correctness of the behavior of an adaptive software system during dynamic adaptation is an important challenge along the way to realize correct adaptive systems. In this research, we model adaptation as a supervisory control problem and synthesize a controller that guides the behavior of a software system during adaptation. The system during adaptation is modeled using a graph transition system and properties to be enforced are specified using an automaton. To ensure correctness, we then synthesize a controller that imposes constraints on the system during adaptation.

Place, publisher, year, edition, pages
International Federation of Automatic Control, 2014
Series
IFAC Proceedings Volumes ; Vol 47, Iss 2
Keywords
Adaptive Software System, Dynamic Adaptation, Behavior Correctness, Formal Methods, Supervisory Controller Synthesis
National Category
Computer Sciences
Research subject
Computer and Information Sciences Computer Science, Computer Science
Identifiers
urn:nbn:se:lnu:diva-42252 (URN)10.3182/20140514-3-FR-4046.00035 (DOI)2-s2.0-84945960523 (Scopus ID)978-3-902823-61-8 (ISBN)
Conference
12th International Workshop on Discrete Event Systems (2014), Cachan, France, 14-15 May, 2014
Available from: 2015-04-13 Created: 2015-04-13 Last updated: 2018-01-11Bibliographically approved
Dam, M., Guanciale, R., Khakpour, N., Nemati, H. & Schwartz, O. (2013). Formal verification of information flow security for a simple arm-based separation kernel. In: Proceedings of the 2013 ACM SIGSAC conference on Computer & communications security: . Paper presented at The 2013 ACM SIGSAC conference on Computer & communications security (pp. 223-234). ACM Press
Open this publication in new window or tab >>Formal verification of information flow security for a simple arm-based separation kernel
Show others...
2013 (English)In: Proceedings of the 2013 ACM SIGSAC conference on Computer & communications security, ACM Press, 2013, p. 223-234Conference paper, Published paper (Refereed)
Abstract [en]

A separation kernel simulates a distributed environment using a single physical machine by executing partitions in isolation and appropriately controlling communication among them. We present a formal verification of information flow security for a simple separation kernel for ARMv7. Previous work on information flow kernel security leaves communication to be handled by model-external means, and cannot be used to draw conclusions when there is explicit interaction between partitions. We propose a different approach where communication between partitions is made explicit and the information flow is analyzed in the presence of such a channel. Limiting the kernel functionality as much as meaningfully possible, we accomplish a detailed analysis and verification of the system, proving its correctness at the level of the ARMv7 assembly. As a sanity check we show how the security condition is reduced to noninterference in the special case where no communication takes place. The verification is done in HOL4 taking the Cambridge model of ARM as basis, transferring verification tasks on the actual assembly code to an adaptation of the BAP binary analysis tool developed at CMU.

Place, publisher, year, edition, pages
ACM Press, 2013
National Category
Computer Sciences
Identifiers
urn:nbn:se:lnu:diva-42251 (URN)10.1145/2508859.2516702 (DOI)978-1-4503-2477-9 (ISBN)
Conference
The 2013 ACM SIGSAC conference on Computer & communications security
Available from: 2015-04-13 Created: 2015-04-13 Last updated: 2018-01-11Bibliographically approved
Khakpour, N., Schwartz, O. & Dam, M. (2013). Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties.. In: Certified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings. Paper presented at Certified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013 (pp. 276-291). Paper presented at Certified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013. Springer
Open this publication in new window or tab >>Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties.
2013 (English)In: Certified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, Springer, 2013, p. 276-291Chapter in book (Refereed)
Abstract [en]

In this paper, we formally verify security properties of the ARMv7 Instruction Set Architecture (ISA) for user mode executions. To obtain guarantees that arbitrary (and unknown) user processes are able to run isolated from privileged software and other user processes, instruction level noninterference and integrity properties are provided, along with proofs that transitions to privileged modes can only occur in a controlled manner. This work establishes a main requirement for operating system and hypervisor verification, as demonstrated for the PROSPER separation kernel. The proof is performed in the HOL4 theorem prover, taking the Cambridge model of ARM as basis. To this end, a proof tool has been developed, which assists the verification of relational state predicates semi-automatically.

Place, publisher, year, edition, pages
Springer, 2013
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8307
National Category
Computer Sciences
Identifiers
urn:nbn:se:lnu:diva-42250 (URN)10.1007/978-3-319-03545-1_18 (DOI)978-3-319-03544-4 (ISBN)
Conference
Certified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013
Available from: 2015-04-13 Created: 2015-04-13 Last updated: 2018-01-11Bibliographically approved
Khakpour, N., Jalili, S., Talcott, C., Sirjani, M. & Mousavi, M. (2012). Formal modeling of evolving self-adaptive systems. Science of Computer Programming, 78(1), 3-26
Open this publication in new window or tab >>Formal modeling of evolving self-adaptive systems
Show others...
2012 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 78, no 1, p. 3-26Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
Elsevier, 2012
National Category
Computer Sciences
Identifiers
urn:nbn:se:lnu:diva-42242 (URN)10.1016/j.scico.2011.09.004 (DOI)
Available from: 2015-04-13 Created: 2015-04-13 Last updated: 2018-01-11Bibliographically approved
Khakpour, N., Jalili, S., Sirjani, M., Goltz, U. & Abolhasanzadeh:, B. (2012). HPobSAM for modeling and analyzing IT Ecosystems: Through a case study. Journal of Systems and Software, 85(12), 2770-2784
Open this publication in new window or tab >>HPobSAM for modeling and analyzing IT Ecosystems: Through a case study
Show others...
2012 (English)In: Journal of Systems and Software, ISSN 0164-1212, E-ISSN 1873-1228, Vol. 85, no 12, p. 2770-2784Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
Elsevier, 2012
National Category
Computer Sciences
Identifiers
urn:nbn:se:lnu:diva-42243 (URN)10.1016/j.jss.2012.03.007 (DOI)
Available from: 2015-04-13 Created: 2015-04-13 Last updated: 2018-01-11Bibliographically approved
Khakpour, N., Jalili, S. & Sirjani, M. (2011). Assuring the Correctness of Large-scale Adaptive Systems. TU Braunschweig
Open this publication in new window or tab >>Assuring the Correctness of Large-scale Adaptive Systems
2011 (English)Report (Other academic)
Abstract [en]

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.

Place, publisher, year, edition, pages
TU Braunschweig, 2011. p. 36
National Category
Computer Sciences
Identifiers
urn:nbn:se:lnu:diva-42333 (URN)
Available from: 2015-04-14 Created: 2015-04-14 Last updated: 2018-01-11Bibliographically approved
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0002-0377-5595

Search in DiVA

Show all publications