Skip to main content

2017 | Buch

Formal Methods and Software Engineering

19th International Conference on Formal Engineering Methods, ICFEM 2017, Xi'an, China, November 13-17, 2017, Proceedings

insite
SUCHEN

Über dieses Buch

This book constitutes the refereed proceedings of the 19th International Conference on Formal Engineering Methods, ICFEM 2017, held in Xi'an, China, in November 2017. The 28 revised full papers presented together with one invited talk and two abstracts of invited talks were carefully reviewed and selected from 80 submissions. The conference focuses on all areas related to formal engineering methods, such as verification and validation, software engineering, formal specification and modeling, software security, and software reliability.

Inhaltsverzeichnis

Frontmatter

Invited Talk

Frontmatter
Towards Customizable CPS: Composability, Efficiency and Predictability
Abstract
Today, many industrial products are defined by software, and therefore customizable by installing new applications on demand - their functionalities are implemented by software and can be modified and extended by software updates. This trend towards customizable products is extending into all domains of IT, including Cyber-Physical Systems (CPS) such as cars, robotics, and medical devices. However, these systems are often highly safety-critical. The current state-of-practice allows hardly any modifications once safety-critical systems are put in operation. This is due to the lack of techniques to preserve crucial safety conditions for the modified system, which severely restricts the benefits of software.
This work aims at new paradigms and technologies for the design and safe software updates of CPS at operation-time – subject to stringent timing constraints, dynamic workloads, and limited resources on complex computing platforms. Essentially there are three key challenges: Composability, Resource-Efficiency and Predictability to enable modular, incremental and safe software updates over system life-time in use. We present research directions to address these challenges: (1) Open architectures and implementation schemes for building composable systems, (2) Fundamental issues in real-time scheduling aiming at a theory of multi-resource (inc. multiprocessor) scheduling, and (3) New-generation techniques and tools for fully separated verification of timing and functional properties of real-time systems with significantly improved efficiency and scalability. The tools shall support not only verification, but also code generation tailored for both co-simulation (interfaced) with existing design tools such as Open Modelica (for modeling and simulation of physical components), and deployment on given computing platforms.
Wang Yi

Contributed Papers

Frontmatter
Modularization of Refinement Steps for Agile Formal Methods
Abstract
The combination of agile methods and formal methods has been recognized as a promising field of research. However, many formal methods rely on a refinement-based development process which poses problems for their integration into agile processes. We consider redundancies within refinement hierarchies as a challenge for the practical application of stepwise refinement and propose superimposition-based modularization of refinement steps as a potential solution. While traditionally, each model in a refinement hierarchy must be developed and maintained separately, our concept allows developers to specify the refinement steps that transform a model into a refined one. We have developed tool support for the language AsmetaL and evaluated our approach by means of a case study. The results indicate a reduction of complexity for the development artifacts in terms of their overall size by 48.6% for the ground model and four refinements. Furthermore, the case study shows that superimposition-based refinement eases the development of alternative refinements for exploratory development and to cope with changing requirements. Thus, we consider this work as a step towards agile formal methods that are tailored to support iterative development, facilitating their incorporation into agile development processes.
Fabian Benduhn, Thomas Thüm, Ina Schaefer, Gunter Saake
Model Checking Pushdown Epistemic Game Structures
Abstract
In this paper, we investigate the problem of verifying pushdown multi-agent systems with imperfect information. As the formal model, we introduce pushdown epistemic game structures (PEGSs), an extension of pushdown game structures with epistemic accessibility relations (EARs). For the specification, we consider extensions of alternating-time temporal logics with epistemic modalities: ATEL, ATEL\(^*\) and AEMC. We study the model checking problems for ATEL, ATEL\(^*\) and AEMC over PEGSs under various imperfect information settings. For ATEL and ATEL\(^*\), we show that size-preserving EARs, a common definition of the accessibility relation in the literature of games over pushdown systems with imperfect information, will render the model checking problem undecidable under imperfect information and imperfect recall setting. We then propose regular EARs, and provide automata-theoretic model checking algorithms with matching low bounds, i.e., EXPTIME-complete for ATEL and 2EXPTIME-complete for ATEL\(^*\). In contrast, for AEMC, we show that the model checking problem is EXPTIME-complete even in the presence of size-preserving EARs.
Taolue Chen, Fu Song, Zhilin Wu
Transforming Timing Requirements into CCSL Constraints to Verify Cyber-Physical Systems
Abstract
The timing requirements of embedded cyber-physical systems (CPS) constrain CPS behaviors made by scheduling analysis. Lack of physical entity properties modeling and the need of scheduling analysis require a systematic approach to specify timing requirements of CPS at the early phase of requirements engineering. In this work, we extend the Problem Frames notations to capture timing properties of both cyber and physical domain entities into Clock Constraint Specification Language (CCSL) constraints which is more explicit that LTL for scheduling analysis. Interpreting them using operational semantics as finite state machines, we are able to transform these timing requirements into CCSL scheduling constraints, and verify their consistency on NuSMV. Our TimePF tool-supported approach is illustrated through the verification of timing requirements for a representative problem in embedded CPS.
Xiaohong Chen, Ling Yin, Yijun Yu, Zhi Jin
A Framework for Multi-view Reconciliation and for Medical Devices Personalization
Abstract
Software product family approaches have found broad adoption in the embedded systems industry, where systems are modelled from several views such as the software view and the hardware view. A view uses the feature perceived only from the view’s perspective. For example, from a hardware view we perceive only the hardware features. Generating the feasible products of the considered family from these views and the constraints imposed on them is called view reconciliation.
The paper presents a mathematical framework to reason on view reconciliation. It articulates this process as a product of sets of product families. We give the conditions under which the product forms a direct product. We also demonstrate that (multi-) view reconciliation is an operation that is indifferent to the order of integrating the views. Finally, we show that personalizing medical devices is a simple view reconciliation operation that gives a direct-product allowing, using projections, the retrieval of any of the involved views from the conciliated view.
Yihai Chen, Bofang Zhang, Ridha Khedri, Huaikou Miao
Compiling Parameterized X86-TSO Concurrent Programs to Cubicle-
Abstract
We present PMCx86, a compiler from x86 concurrent programs to Cubicle-\(\mathcal {W}\), a model checker for parameterized weak memory array-based transition systems. Our tool handles x86 concurrent programs designed to be executed for an arbitrary number of threads and under the TSO weak memory model. The correctness of our approach relies on a simulation result to show that the translation preserves x86-TSO semantics. To show the effectiveness of our translation scheme, we prove the safety of parameterized critical primitives found in operating systems like mutexes and synchronization barriers. To our knowledge, this is the first approach to prove safety of such parameterized x86-TSO programs.
Sylvain Conchon, David Declerck, Fatiha Zaïdi
Improving the Scalability of Automatic Linearizability Checking in SPIN
Abstract
Concurrency in data structures is crucial to the performance of multithreaded programs in shared-memory multiprocessor environments. However, greater concurrency also increases the difficulty of verifying correctness of the data structure. Model checking has been used for verifying concurrent data structures satisfy the correctness condition ‘linearizability’. In particular, ‘automatic’ tools achieve verification without requiring user-specified linearization points. This has several advantages, but is generally not scalable. We examine the automatic checking used by Vechev et al. in their 2009 work to understand the scalability issues of automatic checking in SPIN. We then describe a new, more scalable automatic technique based on these insights, and present the results of a proof-of-concept implementation.
Patrick Doolan, Graeme Smith, Chenyi Zhang, Padmanabhan Krishnan
Verifying Temporal Properties of C Programs via Lazy Abstraction
Abstract
To verify both safety and liveness temporal properties of programs in practice, this paper investigates scalable Linear Temporal Logic (LTL) property verification approach of C programs. We show that the verification target can be accomplished as a scalable lazy abstraction supplemented Counter-Example Guided Abstraction Refinement (CEGAR) based program analysis task. As a result, the scalable lazy abstraction based safety property analysis approaches as well as their mature supporting tools can be reused to verify temporal properties of C programs. We have implemented the proposed approach in TPChecker to verify temporal properties of C programs. Experimental results on benchmark programs show that the proposed approach performs well when verifying non-safety temporal properties of C programs.
Zhao Duan, Cong Tian, Zhenhua Duan
Combining Event-B and CSP: An Institution Theoretic Approach to Interoperability
Abstract
In this paper we present a formal framework designed to facilitate interoperability between the Event-B specification language and the process algebra CSP. Our previous work used the theory of institutions to provide a mathematically sound framework for Event-B, and this enables interoperability with CSP, which has already been incorporated into the institutional framework. This paper outlines a comorphism relationship between the institutions for Event-B and CSP, leveraging existing tool-chains to facilitate verification. We compare our work to the combined formalism Event-B\(\Vert \)CSP and use a supporting example to illustrate the benefits of our approach.
Marie Farrell, Rosemary Monahan, James F. Power
Refinement-Based Modelling and Verification of Design Patterns for Self-adaptive Systems
Abstract
Design patterns are essential for designing complex systems by reusing recurring design principles. Various design patterns were proposed for self-adaptive systems, but their integration into a model-driven design process that, at the same time, provides formal guarantees is still a challenge. This is especially true for self-adaptive design patterns that are generic and abstract enough to provide general solutions that need to be refined prior to their concrete instantiations. In this paper, we present a structured and comprehensible modelling approach for design patterns in the refinement-based process calculus CSP. We formally show crucial properties of them and analyse the refinement-based relationship between their components, which generalises to entire patterns. Based on these analysis results, we are able to provide a first step towards a general, formally well-founded framework providing generic solutions for recurring problems in the management of self-adaptive systems.
Thomas Göthel, Nils Jähnig, Simon Seif
Assertion Generation Through Active Learning
Abstract
Program assertions are useful for many program analysis tasks. They are however often missing in practice. Many approaches have been developed to generate assertions automatically. Existing methods are either based on generalizing from a set of test cases (e.g., Daikon), or based on some forms of symbolic execution. In this work, we develop a novel approach for generating likely assertions automatically based on active learning. Our targets are complex Java programs which are challenging for symbolic execution. Our key idea is to generate candidate assertions based on test cases and then apply active learning techniques to iteratively improve them. We evaluate our approach using two sets of programs, i.e., 425 methods from three popular Java projects from GitHub and 10 programs from the SVComp repository. We evaluate the ‘correctness’ of the assertions either by comparing them with existing assertion-like checking conditions, or by comparing them with the documentation, or by verifying them.
Long H. Pham, Ly Ly Tran Thi, Jun Sun
Detecting Energy Bugs in Android Apps Using Static Analysis
Abstract
Energy bugs in Android apps are defects that can make Android systems waste much energy as a whole. Energy bugs detection in Android apps has become an important issue since smartphones usually operate on a limited amount of battery capacity and the existence of energy bugs may lead to serious drain in the battery power. This paper focuses on detecting two types of energy bugs, namely resource leak and layout defect, in Android apps. A resource leak is a particular type of energy wasting phenomena where an app does not release its acquired resources such as a sensor and GPS. A layout defect refers to a poor layout structure causing more energy consumption for measuring and drawing the layout. In this paper, we present a static analysis technique called SAAD, that can automatically detect energy bugs in a context-sensitive way. SAAD detects the energy bugs by taking an inter-procedural anaysis of an app. For resource leak analysis, SAAD decompiles APK file into Dalvik bytecodes files and then performs resource leak analysis by taking components call relationship analysis, inter-procedure and intra-procedure analysis. For detecting layout defect, SAAD firstly employs Lint to perform some traditional app analysis, then filters energy defects from reported issues. Our experimental result on 64 publicly-available Android apps shows that SAAD can detect energy bugs effectively. The accuracies of detecting resource leak and layout energy defect are \(87.5\%\) and \(78.1\%\) respectively.
Hao Jiang, Hongli Yang, Shengchao Qin, Zhendong Su, Jian Zhang, Jun Yan
A Flexible Approach for Finding Optimal Paths with Minimal Conflicts
Abstract
Complex systems are usually modelled through a combination of structural and behavioural models, where separate behavioural models make it easier to design and understand partial behaviour. When partial models are combined, we need to guarantee that they are consistent, and several automated techniques have been developed to check this. We argue that in some cases it is impossible to guarantee total consistency, and instead we want to find execution paths across such models with minimal conflicts with respect to a certain metric of interest. We present an efficient and scalable solution to find optimal paths through a combination of the theorem prover Isabelle with the constraint solver Z3. Our approach has been inspired by a healthcare problem, namely how to detect conflicts between medications taken by patients with multiple chronic conditions, and how to find preferable alternatives automatically.
Juliana K. F. Bowles, Marco B. Caminati
A Certified Decision Procedure for Tree Shares
Abstract
We develop a certified decision procedure for reasoning about systems of equations over the “tree share” fractional permission model of Dockins et al. Fractional permissions can reason about shared ownership of resources, e.g. in a concurrent program. We imported our certified procedure into the HIP/SLEEK verification system and found bugs in both the previous, uncertified, decision procedure and HIP/SLEEK itself. In addition to being certified, our new procedure improves previous work by correctly handling negative clauses and enjoys better performance.
Xuan-Bach Le, Thanh-Toan Nguyen, Wei-Ngan Chin, Aquinas Hobor
Classification-Based Parameter Synthesis for Parametric Timed Automata
Abstract
Parametric timed automata are designed to model timed systems with unknown parameters, often representing design uncertainties of external environments. In order to design a robust system, it is crucial to synthesize constraints on the parameters, which guarantee the system behaves according to certain properties. Existing approaches suffer from scalability issues. In this work, we propose to enhance existing approaches through classification-based learning. We sample multiple concrete values for parameters and model check the corresponding non-parametric models. Based on the checking results, we form conjectures on the constraint through classification techniques, which can be subsequently confirmed by existing model checkers for parametric timed automata. In order to limit the number of model checker invocations, we actively identify informative parameter values so as to help the classification converge quickly. We have implemented a prototype and evaluated our idea on 24 benchmark systems. The result shows our approach can synthesize parameter constraints effectively and thus improve parametric verification.
Jiaying Li, Jun Sun, Bo Gao, Étienne André
A Verification Framework for Stateful Security Protocols
Abstract
A long-standing research problem is how to efficiently verify security protocols with tamper-resistant global states, especially when the global states evolve unboundedly. We propose a protocol specification framework, which facilitates explicit modeling of states and state transformations. On the basis of that, we develop an algorithm for verifying security properties of protocols with unbounded state-evolving, by tracking state transformation and checking the validity of the state-evolving traces. We prove the correctness of the verification algorithm, implement both of the specification framework and the algorithm, and evaluate our implementation using a number of stateful security protocols. The experimental results show that our approach is both feasible and practically efficient. Particularly, we have found a security flaw on the digital envelope protocol, which cannot be detected with existing security protocol verifiers.
Li Li, Naipeng Dong, Jun Pang, Jun Sun, Guangdong Bai, Yang Liu, Jin Song Dong
A Sliding-Window Algorithm for On-The-Fly Interprocedural Program Analysis
Abstract
Program analysis plays an important role in finding software flaws. Due to dynamic language features like late binding, there are many program analysis problems for which one could not assume a prior program control flow, e.g., Java points-to analysis, the disassembly of binary codes with indirect jumps, etc. In this work, we give a general formalization of such kind of on-the-fly interprocedural program analysis problems, and present a sliding-window algorithm for it in the framework of weighted pushdown systems. Our sliding window algorithm only consists of a series of local static analyses conducted on an arbitrary number of program methods, which does not sacrifice the precision of the whole program analysis at the manageable cost of caching intermediate analysis results during each iteration. We have implemented and evaluated the sliding-window algorithm by instantiating the framework with Java points-to analysis as an application. Our empirical study showed that the analysis based on the sliding-window algorithm always outperforms the whole program analysis on runtime efficiency and scalability.
Xin Li, Mizuhito Ogawa
Exploring Design Alternatives for RAMP Transactions Through Statistical Model Checking
Abstract
Arriving at a mature distributed system design through implementation and experimental validation is a labor-intensive task. This limits the number of design alternatives that can be explored in practice. In this work we use formal modeling with probabilistic rewrite rules and statistical model checking to explore and extend the design space of the RAMP (Read Atomic Multi-Partition) transaction system for large-scale partitioned data stores. Specifically, we formally model in Maude eight RAMP designs, only two of which were previously implemented and evaluated by the RAMP developers; and we analyze their key consistency and performance properties by statistical model checking. Our results: (i) are consistent with the experimental evaluations of the two implemented designs; (ii) are also consistent with conjectures made by the RAMP developers for other unimplemented designs; and (iii) uncover some promising new designs that seem attractive for some applications.
Si Liu, Peter Csaba Ölveczky, Jatin Ganhotra, Indranil Gupta, José Meseguer
An Improved Android Collusion Attack Detection Method Based on Program Slicing
Abstract
Android applications can leak sensitive information through collusion, which gives the smartphone users a great security risk. We propose an Android collusion attack detection method based on control flow and data flow analysis. This method gives analysis of data propagation between different applications firstly. And then, a multi-apps program slice model based on both data and control flow are given. Last, the privacy data leakage paths of multi-apps are computed by reaching-definition analysis. Meanwhile, the criterions of mobile device information leakage edge are redefined according to the correlation of mobile devices. Based on the above principle, we implemented an Android collusion attack sensitive information leakage detection tools called CollusionDetector. Case study is carried out for typical collusion attack scenarios and it can obtain better results than existing tools and methods. Experiments show that the analysis of control flow can more accurately find the path of privacy propagation, and more effectively to identify collusion attacks.
Yunhao Liu, Xiaohong Li, Zhiyong Feng, Jianye Hao
Parameterized Complexity of Resilience Decision for Database Debugging
Abstract
Resilience decision problem plays a fundamental and important role in database debugging, query explanation and error tracing. Resilience decision problem is defined on a database d, given a boolean query q which is true initially, and a constant \(k>0\), it is to decide if there is a fact set res of size no more than k such that query q becomes false after deleting all facts in res. Previous results showed it is NP-hard in many cases. However, we revisit this decision problem, in the light of the recent parametric refinement of complexity theory, provide some new results including negative and positive ones. We show that, there are still some cases intractable if only consider the query size or variable numbers as the parameter.
Dongjing Miao, Zhipeng Cai
Formal Analysis of Linear Control Systems Using Theorem Proving
Abstract
Control systems are an integral part of almost every engineering and physical system and thus their accurate analysis is of utmost importance. Traditionally, control systems are analyzed using paper-and-pencil proof and computer simulation methods, however, both of these methods cannot provide accurate analysis due to their inherent limitations. Model checking has been widely used to analyze control systems but the continuous nature of their environment and physical components cannot be truly captured by a state-transition system in this technique. To overcome these limitations, we propose to use higher-order-logic theorem proving for analyzing linear control systems based on a formalized theory of the Laplace transform method. For this purpose, we have formalized the foundations of linear control system analysis in higher-order logic so that a linear control system can be readily modeled and analyzed. The paper presents a new formalization of the Laplace transform and the formal verification of its properties that are frequently used in the transfer function based analysis to judge the frequency response, gain margin and phase margin, and stability of a linear control system. We also formalize the active realizations of various controllers, like Proportional-Integral-Derivative (PID), Proportional-Integral (PI), Proportional-Derivative (PD), and various active and passive compensators, like lead, lag and lag-lead. For illustration, we present a formal analysis of an unmanned free-swimming submersible vehicle using the HOL Light theorem prover.
Adnan Rashid, Osman Hasan
Policy Dependent and Independent Information Flow Analyses
Abstract
Information Flow Analysis (IFA) aims at detecting illegal flows of information between program entities. “Legality” is therein specified in terms of various security policies. For the analysis, this opens up two possibilities: building generic, policy independent and building specific, policy dependent IFAs. While the former needs to track all dependencies between program entities, the latter allows for a reduced and thus more efficient analysis.
In this paper, we start out by formally defining a policy independent information flow analysis. Next, we show how to specialize this IFA via policy specific variable tracking, and prove soundness of the specialization. We furthermore investigate refinement relationships between policies, allowing an IFA for one policy to be employed for its refinements. As policy refinement depends on concrete program entities, we additionally propose a precomputation of policy refinement conditions, enabling an efficient refinement check for concrete programs.
Manuel Töws, Heike Wehrheim
Improving Probability Estimation Through Active Probabilistic Model Learning
Abstract
It is often necessary to estimate the probability of certain events occurring in a system. For instance, knowing the probability of events triggering a shutdown sequence allows us to estimate the availability of the system. One approach is to run the system multiple times and then construct a probabilistic model to estimate the probability. When the probability of the event to be estimated is low, many system runs are necessary in order to generate an accurate estimation. For complex cyber-physical systems, each system run is costly and time-consuming, and thus it is important to reduce the number of system runs while providing accurate estimation. In this work, we assume that the user can actively tune the initial configuration of the system before the system runs and answer the following research question: how should the user set the initial configuration so that a better estimation can be learned with fewer system runs. The proposed approach has been implemented and evaluated with a set of benchmark models, random generated models, and a real-world water treatment system.
Jingyi Wang, Xiaohong Chen, Jun Sun, Shengchao Qin
Nested Timed Automata with Diagonal Constraints
Abstract
Time constraints are usually used in timed systems to rule on discrete behaviours based on the valuations of clocks. They are categorized into diagonal-free constraints and diagonal constraints. In timed automata, it is well-known that diagonal constraints are just a useful syntax sugar since each diagonal constraint can be encoded into diagonal-free constraints. However, it is yet unknown when recursion is taken into consideration. This paper investigates the decidability results of these systems with diagonal constraints, under the model of nested timed automata (NeTAs). We show that the NeTAs containing a singleton global clock with diagonal constraints are Turing complete, even when the clock assignment is restricted to the clock reset. In comparison, the reachability problem for a subclass, NeTAs without frozen clocks, is decidable under diagonal constraints.
Yuwei Wang, Yunqing Wen, Guoqiang Li, Shoji Yuen
Integration of Metamorphic Testing with Program Repair Methods Based on Adaptive Search Strategies and Program Equivalence
Abstract
Automated program repair (APR) is a promising approach to localize faults and generate patches for program under repair. One of the test suite based APR techniques, a method leveraging Adaptive search strategies and program Equivalence (AE), has been commonly used for program repair. AE assumes the availability of test oracles, which brings the oracle problem to AE repair procedure. Metamorphic Testing (MT) has been introduced to alleviate the test oracle problem, and it tests the correctness of programs through metamorphic relations (MRs) which are relations among multiple inputs and outputs. This paper presents an integration of AE with MT (referred to as AE-MT) to extend the applicability of AE to those applications with oracle problems. To evaluate the repair effectiveness of AE-MT, an empirical study is conducted against IntroClass benchmark. We conclude that AE-MT outperforms AE in terms of success rate, but is of lower repair quality than AE.
Tingting Wu, Yunwei Dong, Tsong Yueh Chen, Mingyue Jiang, Man Lau, Fei-Ching Kuo, Sebastian Ng
Learning Types for Binaries
Abstract
Type inference for Binary codes is a challenging problem due partly to the fact that much type-related information has been lost during the compilation from high-level source code. Most of the existing research on binary code type inference tend to resort to program analysis techniques, which can be too conservative to infer types with high accuracy or too heavy-weight to be viable in practice. In this paper, we propose a new approach to learning types for recovered variables from their related representative instructions. Our idea is motivated by “duck typing”, where the type of a variable is determined by its features and properties. Our approach first learns a classifier from existing binaries with debug information and then uses this classifier to predict types for new, unseen binaries. We have implemented our approach in a tool called BITY and used it to conduct some experiments on a well-known benchmark coreutils (v8.4). The results show that our tool is more precise than the commercial tool Hey-Rays, both in terms of correct types and compatible types.
Zhiwu Xu, Cheng Wen, Shengchao Qin
Inconsistency Analysis of Time-Based Security Policy and Firewall Policy
Abstract
Packet filtering in firewall either accepts or denies packets based upon a set of predefined rules called firewall policy. In recent years, time-based firewall policies are widely used in many firewalls such as CISCO ACLs. Firewall policy is always designed under the instruction of security policy, which is a generic document that outlines the needs for network access permissions. It is difficult to maintain the consistency of normal firewall policy and security policy, not to mention time-based firewall policy and security policy. Even though there are many analysis methods for security policy and firewall policy, they cannot deal with time constraint. To resolve this problem, we firstly represent time-based security policy and firewall policy as logical formulas, and then use satisfiability modulo theories (SMT) solver Z3 to verify them and analyze inconsistency. We have implemented a prototype system to verify our proposed method, experimental results showed the effectiveness.
Yi Yin, Yuichiro Tateiwa, Yun Wang, Yoshiaki Katayama, Naohisa Takahashi
An Algebraic Approach to Automatic Reasoning for NetKAT Based on Its Operational Semantics
Abstract
NetKAT is a network programming language with a solid mathematical foundation. In this paper, we present an operational semantics and show that it is sound and complete with respect to its original axiomatic semantics. We achieve automatic reasoning for NetKAT such as reachability analysis and model checking of temporal properties, by formalizing the operational semantics in an algebraic executable specification language called Maude. In addition, as NetKAT policies are normalizable, two policies are operationally equivalent if and only if they can be converted into the same normal form. We provide a formal way of reasoning about network properties by turning the equivalence checking problem of NetKAT policies into the normalization problem that can be automated in Maude.
Yuxin Deng, Min Zhang, Guoqing Lei
Pareto Optimal Reachability Analysis for Simple Priced Timed Automata
Abstract
We propose Pareto optimal reachability analysis to solve multi-objective scheduling and planing problems using real-time model checking techniques. Not only the makespan of a schedule, but also other objectives involving quantities like performance, energy, risk, cost etc., can be optimized simultaneously in balance. We develop the Pareto optimal reachability algorithm for Uppaal to explore the state-space and compute the goal states on which all objectives will reach a Pareto optimum. After that diagnostic traces are generated from the initial state to the goal states, and Pareto optimal schedules are obtainable from those traces. We demonstrate the usefulness of this new feature by two case studies.
Zhengkui Zhang, Brian Nielsen, Kim Guldstrand Larsen, Gilles Nies, Marvin Stenger, Holger Hermanns
Backmatter
Metadaten
Titel
Formal Methods and Software Engineering
herausgegeben von
Prof. Zhenhua Duan
Luke Ong
Copyright-Jahr
2017
Electronic ISBN
978-3-319-68690-5
Print ISBN
978-3-319-68689-9
DOI
https://doi.org/10.1007/978-3-319-68690-5