Browsing by Author "Germanos, Vasileios"

Now showing 1 - 7 of 7
  • Thumbnail Image
    ItemOpen Access
    Analysing Petri Nets in a Calculus of Context-aware Ambients
    (IEEE, 2020-07-13) Siewe, Francois; Germanos, Vasileios; Zeng, W.
    This paper proposes an approach to analysing and verifying Petri nets using a Calculus of Context-aware Ambients (CCA). We propose an algorithm that transforms a Petri net into a CCA process. This demonstrates that any system that can be specified in Petri nets can also be specified in CCA. Besides, the system can be analysed and verified using the CCA verification tools. We illustrate the practicality of our approach using a case study of the dining cryptographers problem.
  • Thumbnail Image
    ItemOpen Access
    Diagnosability Under Weak Fairness
    (IEEE, 2014-06) Germanos, Vasileios; Haar, Stefan; Khomenko, Victor; Schwoon, Stefan
    In partially observed Petri nets, diagnosis is the task of detecting whether or not the given sequence of observed labels indicates that some unobservable fault has occurred. Diagnosability is an associated property of the Petri net, stating that in any possible execution an occurrence of a fault can eventually be diagnosed. In this paper we consider diagnosability under the weak fairness (WF) assumption, which intuitively states that no transition from a given set can stay enabled forever -- it must eventually either fire or be disabled. We show that a previous approach to WF-diagnosability in the literature has a major flaw, and present a corrected notion. Moreover, we present an efficient method for verifying WF-diagnosability based on a reduction to LTL-X model checking. An important advantage of this method is that the LTL-X formula is fixed -- in particular, the WF assumption does not have to be expressed as a part of it (which would make the formula length proportional to the size of the specification), but rather the ability of existing model checkers to handle weak fairness directly is exploited.
  • Thumbnail Image
    ItemEmbargo
    Diagnosability Under Weak Fairness
    (ACM, 2015-12-08) Germanos, Vasileios; Haar, Stefan; Khomenko, Victor; Schwoon, Stefan
    In partially observed Petri nets, diagnosis is the task of detecting whether the given sequence of observed labels indicates that some unobservable fault has occurred. Diagnosability is an associated property of the Petri net, stating that in any possible execution, an occurrence of a fault can eventually be diagnosed. In this article, we consider diagnosability under the weak fairness (WF) assumption, which intuitively states that no transition from a given set can stay enabled forever—it must eventually either fire or be disabled. We show that a previous approach to WF-diagnosability in the literature has a major flaw and present a corrected notion. Moreover, we present an efficient method for verifying WF-diagnosability based on a reduction to LTL-X model checking. An important advantage of this method is that the LTL-X formula is fixed—in particular, the WF assumption does not have to be expressed as a part of it (which would make the formula length proportional to the size of the specification), but rather the ability of existing model checkers to handle weak fairness directly is exploited.
  • Thumbnail Image
    ItemOpen Access
    Formal verification of robotics navigation algorithms
    (IEEE, 2016-07-17) Germanos, Vasileios; Secco, Emanuele
    BUGs algorithms are navigation algorithms that have been designed to seek of a target in a plane that contains obstacles. Many new navigation algorithms have been inspired from them and their applications can be found in autonomous mobile robots, e.g., self driving vehicles. These algorithms are inspired from insects and are comparable to the motion of ants, which yields motion strategies for the robot that guarantees the elusive target will be detected, if such strategies exist. However, these algorithms have not been formally verified using existing formal verification tools. Therefore, the aim of this paper is to apply model checking for verifying the correctness of BUGs algorithms and draw conclusions for future uses of formal methods in the design and model checking of navigation algorithms.
  • Thumbnail Image
    ItemOpen Access
    Formal verification of secure information flow in cloud computing
    (Elsevier, 2016-04-11) Zeng, W.; Koutny, M.; Watson, P.; Germanos, Vasileios
    Federated cloud systems increase the reliability and reduce the cost of computational support to an organisation. However, the resulting combination of secure private clouds and less secure public clouds impacts on the overall security of the system as applications need to be located within different clouds. In this paper, the entities of a federated cloud system as well as the clouds are assigned security levels of a given security lattice. Then a dynamic flow sensitive security model for a federated cloud system is introduced within which the Bell–LaPadula rules and cloud security rule can be captured. The rest of the paper demonstrates how Petri nets and the associated verification techniques could be used to analyse the security of information flow in federated cloud systems.
  • Thumbnail Image
    ItemOpen Access
    Mapping of the Security Requirements of GDPR and NISD
    (EAI, 2020-10-05) Saqib, Najmudin; Germanos, Vasileios; Zeng, W.; Maglaras, Leandros
    Privacy and information security have consistently been a priority for the European Union lawmaker. This paper investigates the security requirements of the General Data Protection Regulation (GDPR) and the Directive on security of network and information systems (NISD). This investigation incorporates what is unique about the NISD; how it overlaps with existing frameworks; and how security requirements in the GDPR influence the NISD. This mapping of requirements can help businesses and organizations to distinguish possible difficulties that may experience while conforming to GDPR and NISD and help them create a consistent cybersecurity framework and structure new security plans.
  • Thumbnail Image
    ItemEmbargo
    Modelling and Analysis Mobile Systems Using pi-calculus (EFCP)
    (Springer, 2015-11-24) Khomenko, Victor; Germanos, Vasileios
    Reference passing systems, like mobile and reconfigurable systems are common nowadays. The common feature of such systems is the possibility to form dynamic logical connections between the individual modules. However, such systems are very difficult to verify, as their logical structure is dynamic. Traditionally, decidable fragments of π -calculus, e.g. the well-known Finite Control Processes (FCP), are used for formal modelling of reference passing systems. Unfortunately, FCPs allow only ‘global’ concurrency between processes, and thus cannot naturally express scenarios involving ‘local’ concurrency inside a process, such as multicast. In this paper we propose Extended Finite Control Processes (EFCP), which are more convenient for practical modelling. Moreover, an almost linear translation of EFCPs to FCPs is developed, which enables efficient model checking of EFCPs.