首页期刊导航|Formal aspects of computing
期刊信息/Journal information
Formal aspects of computing
Springer-Verlag
Formal aspects of computing

Springer-Verlag

双月刊

0934-5043

Formal aspects of computing/Journal Formal aspects of computingSCIEIISTP
正式出版
收录年代

    Editorial

    Fantechi, AlessandroHaxthausen, Anne E.Woodcock, Jim
    827-827页
      原文链接:
    • NETL
    • NSTL
    • Springer Nature

    Drawing with SAT: four methods and A tool for producing railway infrastructure schematics

    Luteberget, BjornarJohansen, Christian
    829-854页
    查看更多>>摘要：Schematic drawings showing railway tracks and equipment are commonly used to visualize railway operations and to communicate system specifications and construction blueprints. Recent advances in on-line collaboration and modeling tools have raised the expectations for quickly making changes to models, resulting in frequent changes to layouts, text, and/or symbols in schematic drawings. Automating the creation of high-quality schematic views from geographical and topological models can help engineers produce and update drawings efficiently. This paper introduces four methods for automatically producing schematic railway drawings with increasing level of quality and control over the result. The final method, implemented in the open-source tool that we have developed, can use any combination of the following optimization criteria, which can have different priorities in different use cases: width and height of the drawing, the diagonal line lengths, and the number of bends. We show how to encode schematic railway drawings as an optimization problem over Boolean and numerical domains, using combinations of unary number encoding, lazy difference constraints, and numerical optimization into an incremental SAT formulation. We compare drawings resulting from each of the four methods, applied to models of real-world engineering projects and existing railway infrastructure. We also show how to add symbols and labels to the track plan, which is important for the usefulness of the final outputs. Since the proposed tool is customizable and efficiently produces high-quality drawings from railML 2.x models, it can be used (as it is or extended) both as an integrated module in an industrial design tool like RailCOMPLETE, or by researchers for visualization purposes.
      原文链接:
    • NETL
    • NSTL
    • Springer Nature

    Integration of formal proof into unified assurance cases with Isabelle/SACM

    Foster, SimonNemouchi, YakoubGleirscher, MarioWei, Ran...
    855-884页
    查看更多>>摘要：Assurance cases are often required to certify critical systems. The use of formal methods in assurance can improve automation, increase confidence, and overcome errant reasoning. However, assurance cases can never be fully formalised, as the use of formal methods is contingent on models that are validated by informal processes. Consequently, assurance techniques should support both formal and informal artifacts, with explicated inferential links between them. In this paper, we contribute a formal machine-checked interactive language, called Isabelle/SACM, supporting the computer-assisted construction of assurance cases compliant with the OMG Structured Assurance Case Meta-Model. The use of Isabelle/SACM guarantees well-formedness, consistency, and traceability of assurance cases, and allows a tight integration of formal and informal evidence of various provenance. In particular, Isabelle brings a diverse range of automated verification techniques that can provide evidence. To validate our approach, we present a substantial case study based on the Tokeneer secure entry system benchmark. We embed its functional specification into Isabelle, verify its security requirements, and form a modular security case in Isabelle/SACM that combines the heterogeneous artifacts. We thus show that Isabelle is a suitable platform for critical systems assurance.
      原文链接:
    • NETL
    • NSTL
    • Assoc Computing Machinery

    Enhancing probabilistic model checking with ontologies

    Dubslaff, ClemensKoopmann, PatrickTurhan, Anni-Yasmin
    885-921页
    查看更多>>摘要：Probabilistic model checking (PMC) is a well-established method for the quantitative analysis of state based operational models such as Markov decision processes. Description logics (DLs) provide a well-suited formalism to describe and reason about knowledge and are used as basis for the web ontology language (OWL). We investigate how such knowledge described by DLs can be integrated into the PMC process, introducing ontology-mediated PMC. Specifically, we propose ontologized programs as a formalism that links ontologies to behaviors specified by probabilistic guarded commands, the de-facto standard input formalism for PMC tools such as Prism. Through DL reasoning, inconsistent states in the modeled system can be detected. We present three ways to resolve these inconsistencies, leading to different Markov decision process semantics. We analyze the computational complexity of checking whether an ontologized program is consistent under these semantics. Further, we present and implement a technique for the quantitative analysis of ontologized programs relying on standard DL reasoning and PMC tools. This way, we enable the application of PMC techniques to analyze knowledge-intensive systems.We evaluate our approach and implementation on amulti-server systemcase study,where different DL ontologies are used to provide specifications of different server platforms and situations the system is executed in.
      原文链接:
    • NETL
    • NSTL
    • Springer Nature

    Editorial

    Cabot, JordiWehrheim, HeikeBoiten, Eerke
    923-924页
      原文链接:
    • NETL
    • NSTL
    • Springer Nature

    Efficient data validation for geographical interlocking systems

    Peleska, JanKrafczyk, NiklasHaxthausen, Anne E.Pinger, Ralf...
    925-955页
    查看更多>>摘要：In this paper, an efficient approach to data validation of distributed geographical interlocking systems (IXLs) is presented. In the distributed IXL paradigm, track elements are controlled by local computers communicating with other control components over local and wide area networks. The overall control logic is distributed over these track-side computers and remote server computers that may even reside in one or more cloud server farms. Redundancy is introduced to ensure fail-safe behaviour, fault-tolerance, and to increase the availability of the overall system. To cope with the configuration-related complexity of such distributed IXLs, the software is designed according to the digital twin paradigm: physical track elements are associated with software objects implementing supervision and control for the element. The objects communicate with each other and with high-level IXL control components in the cloud over logical channels realised by distributed communication mechanisms. The objective of this article is to explain how configuration rules for this type of IXLs can be specified by temporal logic formulae interpreted on Kripke Structure representations of the IXL configuration. Violations of configuration rules can be specified using formulae from a well-defined subset of LTL. By decomposing the complete configuration model into sub-models corresponding to routes through the model, the LTL model checking problem can be transformed into a CTL checking problem for which highly efficient algorithms exist. Specialised rule violation queries that are hard to express in LTL can be simplified and checked faster by performing sub-model transformations adding auxiliary variables to the states of the underlying Kripke Structures. Further performance enhancements are achieved by checking each sub-model concurrently. The approach presented here has been implemented in a model checking tool which is applied by Siemens Mobility for data validation of geographical IXLs.
      原文链接:
    • NETL
    • NSTL
    • Assoc Computing Machinery

    Analysing an autonomous tramway positioning system with the UPPAAL Statistical Model Checker

    Basile, DavideFantechi, AlessandroRucher, LuigiMando, Gianluca...
    957-987页
    查看更多>>摘要：The substitution of traditional occupancy detecting sensors with an Autonomous Positioning System (APS) is a promising solution to contain costs and improve performance of current tramway signalling systems. APS is an onboard system using satellite positioning and other inertial platforms to autonomously estimate the position of the tram with the needed levels of uncertainty and protection. However, autonomous positioning introduces, even in absence of faults, a quantitative uncertainty with respect to traditional sensors. This paper investigates this issue in the context of an industrial project: a model of the envisaged solution is proposed, and it is analysed using Uppaal Statistical Model Checker. A novel model-driven hazard analysis approach to the exploration of emerging hazards is proposed. The analysis emphasises how the virtualisation of legacy track circuits and on-board satellite positioning equipment may give rise to new hazards, not present in the traditional system.
      原文链接:
    • NETL
    • NSTL
    • Assoc Computing Machinery

    Compositional modeling of railway Virtual Coupling with Stochastic Activity Networks

    Flammini, FrancescoMarrone, StefanoNardone, RobertoVittorini, Valeria...
    989-1007页
    查看更多>>摘要：The current travel demand in railways requires the adoption of novel approaches and technologies in order to increase network capacity. Virtual Coupling is considered one of the most innovative solutions to increase railway capacity by drastically reducing train headway. The aim of this paper is to provide an approach to investigate the potential of Virtual Coupling in railways by composing stochastic activity networks model templates. The paper starts describing the Virtual Coupling paradigm with a focus on standard European railway traffic controllers. Based on stochastic activity network model templates, we provide an approach to perform quantitative evaluation of capacity increase in reference Virtual Coupling scenarios. The approach can be used to estimate system capacity over a modelled track portion, accounting for the scheduled service as well as possible failures. Due to its modularity, the approach can be extended towards the inclusion of safety model components. The contribution of this paper is a preliminary result of the PERFORMINGRAIL (PERformance-based Formal modelling and Optimal tRaffic Management for movING-block RAILway signalling) project funded by the European Shift2Rail Joint Undertaking.
      原文链接:
    • NETL
    • NSTL
    • Assoc Computing Machinery

    A refinement-based development of a distributed signalling system

    Stankaitis, PauliusIliasov, AlexeiKobayashi, TsutomuAit-Ameur, Yamine...
    1009-1036页
    查看更多>>摘要：The decentralised railway signalling systems have a potential to increase capacity, availability and reduce maintenance costs of railway networks. However, given the safety-critical nature of railway signalling and the complexity of novel distributed signalling solutions, their safety should be guaranteed by using thorough system validation methods. To achieve such a high-level of safety assurance of these complex signalling systems, scenario-based testing methods are far from being sufficient despite that they are still widely used in the industry. Formal verification is an alternative approach which provides a rigorous approach to verifying complex systems and has been successfully used in the railway domain. Despite the successes, little work has been done in applying formal methods for distributed railway systems. In our research we are working towards a multifaceted formal development methodology of complex railway signalling systems. The methodology is based on the Event-B modelling language which provides an expressive modelling language, a stepwise development and a proof-based model verification. In this paper, we present the application of the methodology for the development and verification of a distributed protocol for reservation of railway sections. The main challenge of this work is developing a distributed protocol which ensures safety and liveness of the distributed railway system when message delays are allowed in the model.
      原文链接:
    • NETL
    • NSTL
    • Springer Nature

    Editorial

    Ahrendt, WolfgangTapia Tarifa, Silvia LizethWehrheim, Heike
    1037-1037页
      原文链接:
    • NETL
    • NSTL
    • Springer Nature