Labelled transition systems(LTSs) are widely used to formally describe system behaviour.The labels of LTS are extended to offer a more satisfactory description of behaviour by refining the abstract labels into multiva...Labelled transition systems(LTSs) are widely used to formally describe system behaviour.The labels of LTS are extended to offer a more satisfactory description of behaviour by refining the abstract labels into multivariate polynomials.These labels can be simplified by numerous numerical approximation methods.Those LTSs that can not apply failures semantics equivalence in description and verification may have a chance after using approximation on labels.The technique that combines approximation and failures semantics equivalence effectively alleviates the computational complexity and minimizes LTS.展开更多
This paper adopts counterexample guided abstraction refinement scheme to alleviate the state explosion problem of deadlock detection. We extend the classical labeled transition system models by qualifying transitions ...This paper adopts counterexample guided abstraction refinement scheme to alleviate the state explosion problem of deadlock detection. We extend the classical labeled transition system models by qualifying transitions as certain and uncertain to make deadlock-freedom conservative, i.e. if the abstraction of a system is deadlock-free, then the system is deadlock-free. An abstraction refinement approach to deadlock detection is proposed, and the correctness of the approach is proved.展开更多
In this paper, a labelled transition semantics for higher-order processcalculi is studied. The labelled transition semantics is relatively clean and simple, andcorresponding bisimulation equivalence can be easily form...In this paper, a labelled transition semantics for higher-order processcalculi is studied. The labelled transition semantics is relatively clean and simple, andcorresponding bisimulation equivalence can be easily formulated based on it. And the congruenceproperties of the bisimulation equivalence can be proved easily. To show the correspondence betweenthe proposed semantics and the well-established ones, the bisimulation is characterized as a versionof barbed equivalence and a version of context bisimulation.展开更多
Checking if the implementations conform to the requirement models is challenging. Most existing techniques for consistency checking either focus on requirement models（e.g., requirements consistency checking）, or on ...Checking if the implementations conform to the requirement models is challenging. Most existing techniques for consistency checking either focus on requirement models（e.g., requirements consistency checking）, or on the implementations（e.g., code-based testing） only. In this paper we propose an approach to checking behavioral consistency of implementations against requirement models directly to overcome these limitations. Our approach extracts two behavioral models represented by Labelled Transition Systems（LTS） from requirement models and implementations respectively, and checks the behavioral consistency between these two models based on behavioral simulation relation of LTS. The checking results of our approach provide evidence for behavioral inconsistency as well as inconsistent localization. A research prototype called BCCH and a case study are presented to give initial validation of this approach.展开更多
基金National Natural Science Foundation of China(No.11371003)Natural Science Foundations of Guangxi,China(No.2011GXNSFA018154,No.2012GXNSFGA060003)+2 种基金Science and Technology Foundation of Guangxi,China(No.10169-1)Scientific Research Project from Guangxi Education Department,China(No.201012MS274)Open Research Fund Program of Guangxi Key Laboratory of Hybrid Computation and IC Design Analysis,China(No.HCIC201301)
文摘Labelled transition systems(LTSs) are widely used to formally describe system behaviour.The labels of LTS are extended to offer a more satisfactory description of behaviour by refining the abstract labels into multivariate polynomials.These labels can be simplified by numerous numerical approximation methods.Those LTSs that can not apply failures semantics equivalence in description and verification may have a chance after using approximation on labels.The technique that combines approximation and failures semantics equivalence effectively alleviates the computational complexity and minimizes LTS.
基金supported by the Natural Science Foundation of Shanghai (Grant No.09ZR1412100)the National Natural Science Foundation of China (Grant No.60673115)the Shanghai Leading Academic Discipline Project (Grant No.J50103)
文摘This paper adopts counterexample guided abstraction refinement scheme to alleviate the state explosion problem of deadlock detection. We extend the classical labeled transition system models by qualifying transitions as certain and uncertain to make deadlock-freedom conservative, i.e. if the abstraction of a system is deadlock-free, then the system is deadlock-free. An abstraction refinement approach to deadlock detection is proposed, and the correctness of the approach is proved.
文摘In this paper, a labelled transition semantics for higher-order processcalculi is studied. The labelled transition semantics is relatively clean and simple, andcorresponding bisimulation equivalence can be easily formulated based on it. And the congruenceproperties of the bisimulation equivalence can be proved easily. To show the correspondence betweenthe proposed semantics and the well-established ones, the bisimulation is characterized as a versionof barbed equivalence and a version of context bisimulation.
基金Supported by the National Natural Science Foundation of China(91118003,61003071)the Fundamental Research Funds for the Central Universities(3101046,201121102020006)the Special Funds for Shenzhen Strategic New Industry Development(JCYJ20120616135936123)
文摘Checking if the implementations conform to the requirement models is challenging. Most existing techniques for consistency checking either focus on requirement models（e.g., requirements consistency checking）, or on the implementations（e.g., code-based testing） only. In this paper we propose an approach to checking behavioral consistency of implementations against requirement models directly to overcome these limitations. Our approach extracts two behavioral models represented by Labelled Transition Systems（LTS） from requirement models and implementations respectively, and checks the behavioral consistency between these two models based on behavioral simulation relation of LTS. The checking results of our approach provide evidence for behavioral inconsistency as well as inconsistent localization. A research prototype called BCCH and a case study are presented to give initial validation of this approach.
