lnu.sePublications
Change search
Refine search result
1 - 28 of 28
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Rows per page
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sort
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
Select
The maximal number of hits you can export is 250. When you want to export more records please use the Create feeds function.
  • 1.
    Bagheri, Maryam
    et al.
    Sharif University Of Technology, Iran.
    Akkaya, Ilge
    University of California at Berkeley, USA.
    Khamespanah, Ehsan
    University of Tehran, Iran ; Reykjavik University, Iceland.
    Khakpour, Narges
    Linnaeus University, Faculty of Technology, Department of Computer Science.
    Sirjani, Marjan
    Reykjavik University, Iceland ; Mälardalen University.
    Movaghar, Ali
    Sharif University Of Technology, Iran.
    Lee, Edward A.
    University of California at Berkeley, USA.
    Coordinated actors for reliable self-adaptive systems2017In: FACS 2016 : Formal Aspects of Component Software: International Workshop on Formal Aspects of Component Software, Springer, 2017, p. 241-259Conference 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.

  • 2.
    Bagheri, Maryam
    et al.
    Sharif Univ Technol, Iran.
    Sirjani, Marjan
    Mälardalen University;Reykjavik Univ, Iceland.
    Khamespanah, Ehsan
    Reykjavik Univ, Iceland;Univ Tehran, Iran.
    Khakpour, Narges
    Linnaeus University, Faculty of Technology, Department of computer science and media technology (CM).
    Akkaya, Ilge
    Univ Calif Berkeley, USA.
    Movaghar, Ali
    Sharif Univ Technol, Iran.
    Lee, Edward A.
    Univ Calif Berkeley, USA.
    Coordinated actor model of self-adaptive track-based traffic control systems2018In: Journal of Systems and Software, ISSN 0164-1212, E-ISSN 1873-1228, Vol. 143, p. 116-139Article in journal (Refereed)
    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.

  • 3.
    Caporuscio, Mauro
    et al.
    Linnaeus University, Faculty of Technology, Department of computer science and media technology (CM).
    Flammini, Francesco
    Linnaeus University, Faculty of Technology, Department of computer science and media technology (CM).
    Khakpour, Narges
    Linnaeus University, Faculty of Technology, Department of computer science and media technology (CM).
    Singh, Prasannjeet
    Linnaeus University, Faculty of Technology, Department of computer science and media technology (CM).
    Thornadtsson, Johan
    Sigma Technology, Sweden.
    Smart-troubleshooting connected devices: Concept, challenges and opportunities2019In: Future generations computer systems, ISSN 0167-739X, E-ISSN 1872-7115Article in journal (Refereed)
    Abstract [en]

    Today’s digital world and evolving technology has improved the quality of our lives but it has also come with a number of new threats. In the society of smart-cities and Industry 4.0, where many cyber-physical devices connect and exchange data through the Internet of Things, the need for addressing information security and solve system failures becomes inevitable. System failures can occur because of hardware failures, software bugs or interoperability issues. In this paper we introduce the industry-originated concept of “smart-troubleshooting” that is the set of activities and tools needed to gather failure information generated by heterogeneous connected devices, analyze them, and match them with troubleshooting instructions and software fixes. As a consequence of implementing smart-troubleshooting, the system would be able to self-heal and thus become more resilient. This paper aims to survey frameworks, methodologies and tools related to this new concept, and especially the ones needed to model, analyze and recover from failures in a (semi)automatic way. Smart-troubleshooting has a relation with event analysis to perform diagnostics and prognostics on devices manufactured by different suppliers in a distributed system. It also addresses management of appropriate product information specified in possibly unstructured formats to guide the troubleshooting workflow in identifying fault–causes and solutions. Relevant research is briefly surveyed in the paper in order to highlight current state-of-the-art, open issues, challenges to be tackled and future opportunities in this emerging industry paradigm.

  • 4.
    Dam, Mads
    et al.
    KTH Royal Institute of Technology.
    Guanciale, Roberto
    KTH Royal Institute of Technology.
    Khakpour, Narges
    KTH Royal Institute of Technology.
    Nemati, Hamed
    KTH Royal Institute of Technology.
    Schwartz, Oliver
    SICS Swedish ICT.
    Formal verification of information flow security for a simple arm-based separation kernel2013In: Proceedings of the 2013 ACM SIGSAC conference on Computer & communications security, ACM Press, 2013, p. 223-234Conference 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.

  • 5.
    Goltz, Ursula
    et al.
    NTH School for IT Ecosystems, Germany.
    Khakpour, Narges
    NTH School for IT Ecosystems, Germany.
    Knieke, Christoph
    NTH School for IT Ecosystems. Germany.
    Martin, Lukas
    NTH School for IT Ecosystems, Germany.
    Behavioral Modeling of IT Ecosystems2010Report (Other academic)
    Abstract [en]

    IT ecosystems - systems composed of a large number of distributed, autonomous, cooperating, decentralized, interacting, organically grown, heterogeneous, and continually evolving subsystems - are the future system generation. Today’s state of the art does not enable us to develop these systems. Within the NTH Focused Research School for IT Ecosystems, research project AIM deals with methods and tools to guarantee the functionality of a complex IT ecosystem especially when a top-down design is not possible anymore. Thus, adaptive information- and collaboration architectures considering independent evolution of subsystems as well as suitable control mechanisms are examined. This technical report analyzes how adaptive behavior of subsystems can be modeled adequately by standard formalisms for behavioral modeling (e.g. UML) as well as advanced approaches for modeling adaptive behavior (e.g. PobSAM). We apply the selected modeling languages on a fictional case study, an airport departure scenario. The smart airport itself can be seen as an IT ecosystem due to the complexity of the interacting systems.

  • 6. Jalili, Saeed
    et al.
    Khakpour, Narges
    Verication of Service Access Control Policies: A Description Logic Approach2006Conference paper (Refereed)
  • 7. Khakpour, Narges
    A Formal Model to Develop and Verify Self-Adaptive Systems2009In: Proceedings of Formal Methods 2009 Doctoral Symposium: November 6, 2009 / [ed] MohammadReza Mousavi and Emil Sekerinski, Technische Universiteit Eindhoven, 2009, p. 20-25Conference paper (Refereed)
  • 8.
    Khakpour, Narges
    Linnaeus University, Faculty of Technology, Department of computer science and media technology (CM), Department of Computer Science.
    Control of Self-adaptation Under Partial Observation: A Modular Approach2017In: Software Architecture: 11th European Conference, ECSA 2017, Canterbury, UK, September 11-15, 2017, Proceedings / [ed] Antónia Lopes & Rogério de Lemos, Springer, 2017, Vol. 10475, p. 112-119Conference paper (Refereed)
    Abstract [en]

    To realize correct adaptive and reconfigurable systems, we need techniques to assure that the behavior of an adaptive system during dynamic adaptation is correct. In this paper, we propose a modular approach to synthesize a symbolic reconfiguration controller that guides the behavior of a system during adaptation under partial observations. The reconfiguration controller observes the system behavior partially during an adaptation and controls it by allowing/disallowing actions in a way to ensure that a given property is satisfied and a deadlock is avoided.

  • 9.
    Khakpour, Narges
    et al.
    Linnaeus University, Faculty of Technology, Department of computer science and media technology (CM), Department of Computer Science. Leiden University, The Netherlands.
    Arbab, Farhad
    Leiden University, The Netherlands.
    Rutten, Eric
    INRIA, France.
    Supervisory Controller Synthesis for Safe Software Adaptation2014In: 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 (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.

  • 10.
    Khakpour, Narges
    et al.
    Linnaeus University, Faculty of Technology, Department of Computer Science. Leiden University, The Netherlands.
    Arbab, Farhad
    Leiden University, The Netherlands ; CWI, The Netherlands.
    Rutten, Eric
    INRIA, France.
    Synthesizing structural and behavioral control for reconfigurations in component-based systems2016In: Formal Aspects of Computing, ISSN 0934-5043, E-ISSN 1433-299X, Vol. 28, no 1, p. 21-43Article in journal (Refereed)
    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.

  • 11. Khakpour, Narges
    et al.
    Jalili, Saeed
    A Formal Approach for Analysis of Distributed Firewalls Congurations2007Conference paper (Refereed)
  • 12.
    Khakpour, Narges
    et al.
    Tarbiat Modares University, Iran.
    Jalili, Saeed
    Tarbiat Modares University, Iran.
    Using Supervised and Transductive Learning Techniques to Extract Network Attack Scenarios2009In: 14th International CSI, Computer Conference, CSICC 2009, IEEE, 2009, p. 71-76Conference paper (Refereed)
    Abstract [en]

    Intrusion detection can no longer satisfy security needs of an organization solely. Recently, the attention of security community turned to automatic intrusion response and prevention, as the techniques, to protect network resources as well as to reduce the attack damages. Knowing attack scenarios enables the system administrator to respond to the threats swiftly by either blocking the attacks or preventing them from escalating. Alert correlation is a technique to extract attack scenarios by investigating the correlation of intrusion detection systems alerts. In this paper, we propose a new learning-based method for alert correlation that employs supervised and transductive learning techniques. Using this method, we are able to extract attack scenarios automatically.

  • 13.
    Khakpour, Narges
    et al.
    Tarbiat Modares University, Iran.
    Jalili, Saeed
    Tarbiat Modares University, Iran.
    Verification of Distributed Firewalls Configuration vs. Security Policies Using ALCQI(d)2009In: Applied Artificial Intelligence, ISSN 0883-9514, E-ISSN 1087-6545, Vol. 23, no 10, p. 945-975Article in journal (Refereed)
    Abstract [en]

    Packet filtering firewalls have an important role in providing security in IP networks which control the traversal of packets across the boundaries of a secured network based on a specific security policy. Manual configuring of packet filtering firewalls can be extremely complex and error-prone. Therefore, it can be performed in an improper way which is not in conformance with security policies. So, we need an approach to analyze the configuration of whole packet-filtering firewalls in the network in order to discover all policy violations. In this article, we introduce an approach based on description logics to verify the configuration of all the firewalls in a network universally vs. security policies. Using this approach, system managers can express and analyze security policies with a formal and simple language. This high-level language is extensible and topology-independent. In this approach, we first automatically transform high-level security policies into low-level policies, i.e., filtering rules. Then we develop an algorithm to discover policy violations which takes configuration of the firewalls, network topology, routing information, and low-level security policies as input and determines existing policy violations as output.

  • 14.
    Khakpour, Narges
    et al.
    TU Braunschweig, Germany.
    Jalili, Saeed
    Tarbiat Modares University, Iran.
    Sirjani, Marjan
    Reykjavik University, Iceland.
    Assuring the Correctness of Large-scale Adaptive Systems2011Report (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.

  • 15.
    Khakpour, Narges
    et al.
    Technical University of Braunschweig, Germany.
    Jalili, Saeed
    Tarbiat Modares University, Iran.
    Sirjani, Marjan
    Reykjavk University, Iceland.
    Goltz, Ursula
    Technical University of Braunschweig, Germany.
    Abolhasanzadeh:, Bahareh
    Tarbiat Modares University, Iran.
    HPobSAM for modeling and analyzing IT Ecosystems: Through a case study2012In: Journal of Systems and Software, ISSN 0164-1212, E-ISSN 1873-1228, Vol. 85, no 12, p. 2770-2784Article in journal (Refereed)
    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.

  • 16.
    Khakpour, Narges
    et al.
    Tarbiat Modares University, Iran.
    Jalili, Saeed
    Tarbiat Modares University, Iran.
    Talcott, Carolyn
    SRI International, United States.
    Sirjani, Marjan
    Reykjavík University, Iceland.
    Mousavi, MohammadReza
    Eindhoven University of Technology, The Netherlands.
    Formal modeling of evolving self-adaptive systems2012In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 78, no 1, p. 3-26Article in journal (Refereed)
    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.

  • 17.
    Khakpour, Narges
    et al.
    Tarbiat Modares University, Iran.
    Jalili, Saeed
    Tarbiat Modares University, Iran.
    Talcott, Carolyn
    SRI International, California.
    Sirjani, Marjan
    Reykjavk University, Iceland.
    Mousavi, MohammadReza
    Eindhoven University of Technology, The Netherlands.
    PobSAM: Policy-based Managing of Actors in Self-Adaptive Systems2010In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, E-ISSN 1571-0661, Vol. 263, p. 129-143Article in journal (Refereed)
    Abstract [en]

    In this paper, we present a formal model, named PobSAM (Policy-based Self-Adaptive Model), for developing and modeling self-adaptive systems. In this model, policies are used as a mechanism to direct and adapt the behavior of self-adaptive systems. A PobSAM model consists of a set of self-managed modules(SMM). An SMM is a collection of autonomous managers and managed actors. Managed actors are dedicated to functional behavior while autonomous managers govern the behavior of managed actors by enforcing suitable policies. To adapt SMM behavior in response to changes, policies governing an SMM are adjusted, i.e., dynamic policies are used to govern and adapt system behavior. We employ the combination of an algebraic formalism and an actor-based model to specify this model formally. Managers are modeled as meta-actors whose policies are described using an algebra. Managed actors are expressed by an actor model. Furthermore, we provide an operational semantics for PobSAM described using labeled transition systems.

  • 18.
    Khakpour, Narges
    et al.
    Tarbiat Modares University, Iran.
    Khosravi, Ramtin
    University of Tehran, Iran.
    Sirjani, Marjan
    University of Tehran, Iran.
    Jalili, Saeed
    Tarbiat Modares University, Iran.
    Formal analysis of policy-based self-adaptive systems2010In: Proceedings of the 2010 ACM Symposium on Applied Computing, SAC'10, ACM Press, 2010, p. 2536-2543Conference paper (Refereed)
    Abstract [en]

    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.

  • 19.
    Khakpour, Narges
    et al.
    Linnaeus University, Faculty of Technology, Department of computer science and media technology (CM).
    Klein, Jetty
    Leiden University, Netherlands.
    Sirjani, Marjan
    Mälardalen University, Sweden.
    A formal model to integrate behavioral and structural adaptations in self-adaptive systems2019In: Fundamentals of software engineering: 8th International conference, FSEN 2019, Tehran, Iran, May 1-3, 2019, Revised selected papers / [ed] Hossein Hojjat & Mieke Massink, Springer, 2019, Vol. 11761, p. 3-19Chapter in book (Refereed)
    Abstract [en]

    An approach for modelling adaptive complex systems should be flexible and scalable to allow a system to grow easily, and should have a formal foundation to guarantee the correctness of the system behavior. In this paper, we present the architecture, and formal syntax and semantics of HPobSAM which is a model for specifying behavioral and structural adaptations to model large-scale systems and address re-usability concerns. Self-adaptive modules are used as the building blocks to structure a system, and policies are used as the mechanism to perform both behavioral and structural adaptations. While a self-adaptive module is autonomous to achieve its local goals by collaborating with other self-adaptive modules, it is controlled by a higher-level entity to prevent undesirable behavior. HPobSAM is formalized using a combination of algebraic, graph transformation-based and actor-based formalisms.

  • 20.
    Khakpour, Narges
    et al.
    Linnaeus University, Faculty of Technology, Department of Computer Science.
    Mousavi, Mohammad Reza
    Halmstad University.
    Notions of Conformance Testing for Cyber-Physical Systems: Overview and Roadmap2015In: 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 (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.

  • 21.
    Khakpour, Narges
    et al.
    KTH Royal Institute of Technology.
    Schwartz, Oliver
    SICS.
    Dam, Mads
    KTH Royal Institute of Technology.
    Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties.2013In: 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.

  • 22.
    Khakpour, Narges
    et al.
    Technical University of Braunschweig, Germany.
    Sirjani, Marjan
    Reykjavik University, Iceland.
    Goltz, Ursula
    Technical University of Braunschweig, Germany.
    Context-Based Behavioral Equivalence of Components in Self-Adaptive Systems2011In: Formal Methods and Software Engineering. 13th International Conference on Formal Engineering Methods (ICREM 2011). Durham, UK, 20111026, Springer, 2011, p. 16-32Conference paper (Refereed)
    Abstract [en]

    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.

  • 23. Khakpour, Narges
    et al.
    Sirjani, Marjan
    Jalili, Saeed
    Formal Analysis of Smart Home Policies using Compositional Verification2009Conference paper (Refereed)
    Abstract [en]

    Smart spaces contain a large number of computing devices communicating with each other to perform various high-order tasks. They are governed by predefined policies that users can put according to their preferences. In this paper, we investigate the policy interaction problem beyond the smart home domain. We use a formal method for detecting dynamic conflicts between policies. First, we give an abstract model of the system described with an actor-based language. Then, we identify different kinds of conflicts that may exist among policies in smart home domain. To reduce the complexity of model checking, we use compositional verification as well as data abstraction techniques.

  • 24.
    Khakpour, Narges
    et al.
    Linnaeus University, Faculty of Technology, Department of computer science and media technology (CM).
    Skandylas, Charilaos
    Linnaeus University, Faculty of Technology, Department of computer science and media technology (CM).
    Synthesis of a Permissive Security Monitor2018In: Computer Security - 23rd European Symposium on Research in Computer Security, ESORICS 2018, Barcelona, Spain, September 3-7, 2018, Proceedings, Part I / [ed] Lopez, J; Zhou, J; Soriano, M, Springer, 2018, Vol. 11098, p. 48-65Conference paper (Refereed)
    Abstract [en]

    In this paper, we propose a new sound method to synthesize a permissive monitor using boolean supervisory controller synthesis that observes a Java program at certain checkpoints, predicts information flow violations and applies suitable countermeasures to prevent violations. To improve the permissiveness, we train the monitor and remove false positives by executing the program along with its executable model. If a security violation is detected, the user can define sound countermeasures, including declassification to apply in the checkpoints. We implement a tool that automates the whole process and generates a monitor. We evaluate our method by applying it on the Droidbench benchmark and one real-life Android application.

  • 25.
    Khakpour, Narges
    et al.
    Linnaeus University, Faculty of Technology, Department of computer science and media technology (CM).
    Skandylas, Charilaos
    Linnaeus University, Faculty of Technology, Department of computer science and media technology (CM).
    Goran, Saman Nariman
    University of Human Development, Iraq.
    Weyns, Danny
    Linnaeus University, Faculty of Technology, Department of computer science and media technology (CM). Catholic University of Leuven, Belgium.
    Towards secure architecture-based adaptations2019In: 2019 IEEE/ACM 14th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS), IEEE, 2019, p. 114-125Conference paper (Refereed)
    Abstract [en]

    As any software system, a self-adaptive system is subject to security threats. However, applying self-adaptation may introduce additional threats. So far, little research has been devoted to this important problem. In this paper, we propose an approach for vulnerability analysis of architecture-based adaptations in self-adaptive systems using threat modeling and analysis techniques. To this end, we specify components' vulnerabilities and the system architecture formally and generate an attack model that describes the attacker's strategies to attack the system by exploiting different vulnerabilities. We use a set of security metrics to quantitatively assess the security risks of adaptations based on the produced attack model which enables the system to consider security aspects while choosing an adaptation to apply to the system. We automate and incorporate our approach into the Rainbow framework, allowing for secure architectural adaptations at runtime. To evaluate the effectiveness of our approach, we apply it on a simple document storage system and on the ZNN system.

  • 26.
    Khaksar, Mohsen
    et al.
    Univ Tarbiat Modares, Iran.
    Jalili, Saeed
    Univ Tarbiat Modares, Iran.
    Khakpour, Narges
    Univ Tarbiat Modares, Iran.
    Shaban Jokhio, S
    The University of Auckland, New Zealand.
    Monitoring safety properties of composite web services at runtime using CSP2009In: 13th Enterprise Distributed Object Computing Conference Workshops, 2009. EDOCW 2009, IEEE, 2009, p. 107-113Conference paper (Refereed)
    Abstract [en]

    Nowadays, service oriented architecture has been given strong attention as an important approach to integrate heterogeneous systems, in which complex services are created by composing simplerservices offered by various systems. The correctness of composition requires techniques to verify if the composite service behaves properly. To this end, in this paper we propose a new method forruntime monitoring of composite services which uses Communicating Sequential Processes (CSP) to specify properties formally. Then, the CSP specification of properties is translated to a Labeled Transition System (LTS). In order to verify the safety of a composite service, we traverse the generated LTS at runtime. Existing methods almost use temporal logic to specify safety properties. There are two advantages in using CSP: 1) similarity of CSP operators and service composition patterns makes CSPstraightforward to be used by users. 2) there are some properties which can not be specified by temporal logic, while they can be expressed using CSP.

  • 27.
    Skandylas, Charilaos
    et al.
    Linnaeus University, Faculty of Technology, Department of computer science and media technology (CM).
    Khakpour, Narges
    Linnaeus University, Faculty of Technology, Department of computer science and media technology (CM).
    Andersson, Jesper
    Linnaeus University, Faculty of Technology, Department of computer science and media technology (CM).
    Self-Adaptive Trust-aware Decentralized Information Flow Control, extended version2020Report (Other academic)
    Abstract [en]

    Modern software systems and their corresponding architectures are decentralized, distributed, and dynamic. As a consequence, decentralized mechanisms are also required to ensure security in such architectures. Decentralized Information Flow Control (DIFC) is a mechanism to control information flow in distributed systems. However, DIFC mechanisms require the resolution of specific centralized control and trust issues.In this paper, we propose an adaptive, trust-aware, decentralized information flow approach that incorporates trust in DIFC for decentralized systems. We employ decentralized feedback loops to enable decentralized control and adaptive trust assignments. In our approach, adaptivity mitigates two aspects of systems dynamics that cause uncertainty:  the ever-changing nature of trust and the system openness. We formalize our trust-aware DIFC model and instantiate two decentralized feedback loop architectures to implement it.

    Download full text (pdf)
    Self-Adaptive Trust-Aware DecentralizedInformation Flow Control - Technical Report
  • 28.
    Zeller, Silvan
    et al.
    Omegapoint AB, Sweden.
    Khakpour, Narges
    Linnaeus University, Faculty of Technology, Department of computer science and media technology (CM).
    Weyns, Danny
    Linnaeus University, Faculty of Technology, Department of computer science and media technology (CM). Catholic University of Leuven, Belgium.
    Deogun, Daniel
    Omegapoint AB, Sweden.
    Self-protection against business logic vulnerabilities2020In: 15th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS@ICSE 2020), IEEE, 2020, p. 1-7Conference paper (Refereed)
1 - 28 of 28
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf