|
|
|
题名
|
作者
|
年代
|
出处
|
被引量
|
| 1 | Behavior modeling and verification of movement authority scenario of Chinese Train Control System using AADL显示文摘Train control systems like most digital controllers are, by definition, hybrid systems as they interact with or try to control some aspects of the physical world. Detailed behavior modeling with constraints specification and formal verification, required for reliability prediction, is a great challenge for hybrid system designers.Train control systems further intensify this challenge with extensive interaction between computing units and their physical environment and their mutual dependence on each other. In this paper, we investigate behavior modeling and formal verification of Chinese Train Control System Level 3(CTCS-3) using Architectural Analysis & Design Language(AADL) to cope with this challenge. AADL is an architecture description language for embedded systems and is based on model-based engineering paradigm. Along with structural modeling of embedded systems using the core language constructs, AADL also provides support for language extension through annex sublanguages. In system requirements specification document, the behavior of the CTCS-3 is specified as a set of basic operation scenarios that cooperate with each other to achieve safe and secure functionality of trains.Movement Authority(MA) scenario, explored in this paper, is considered as a basic and most crucial scenario to prevent trains from colliding with each other. The detailed discrete behavior of control system is modeled and verified using the Behavior Language for Embedded Systems with Software(BLESS) annex sublanguage of AADL, and the continuous behavior of train with the cyber–physical interaction(communication between train and control system) is modeled using the Hybrid annex sublanguage. The behavior of the MA scenario at system level is verified using the Hybrid Hoare Logic theorem prover. Behavior constraints are specified as assertions using first-order logic formulas augmented with a simple temporal operator. | AHMAD Ehsan DONG YunWei LARSON Brian Lü JiDong TANG Tao ZHAN NaiJun | 2015 | Science China(Information Sciences)2015，58，11： | 4 |
| 2 | Generating Semi-Algebraic Invariants for Non-Autonomous Polynomial Hybrid Systems显示文摘Hybrid systems are dynamical systems with interacting discrete computation and continuous physical processes, which have become more common, more indispensable, and more complicated in our modern life. Particularly, many of them are safety-critical, and therefore are required to meet a critical safety standard. Invariant generation plays a central role in the verification and synthesis of hybrid systems. In the previous work, the fourth author and his coauthors gave a necessary and sufficient condition for a semi-algebraic set being an invariant of a polynomial autonomous dynamical system, which gave a confirmative answer to the open problem. In addition, based on which a complete algorithm for generating all semi-algebraic invariants of a given polynomial autonomous hybrid system with the given shape was proposed. This paper considers how to extend their work to non-autonomous dynamical and hybrid systems. Non-autonomous dynamical and hybrid systems are with inputs, which are very common in practice; in contrast, autonomous ones are without inputs. Furthermore, the authors present a sound and complete algorithm to verify semi-algebraic invariants for non-autonomous polynomial hybrid systems. Based on which, the authors propose a sound and complete algorithm to generate all invariants with a pre-defined template. | WANG Qiuye LI Yangjia XIA Bican ZHAN Naijun | 2017 | Journal of Systems Science & Complexity2017，30，1： | 1 |
| 3 | Symbolic decision procedure for termination of linear programs显示文摘 | Bican Xia Lu Yang Naijun Zhan | 2011 | Formal Aspects of Computing2011，23，2： | 1 |
| 4 | Recent advances in program verification through computer algebra显示文摘 | Lu Yang Chaochen Zhou Naijun Zhan Bican Xia | 2010 | Frontiers of Computer Science in China2010，，1： | 1 |
| 5 | From model to implementation: a network algorithm programming language显示文摘Software-defined networking(SDN) is a revolutionary technology that facilitates network management and enables programmatically efficient network configuration,thereby improving network performance and flexibility.However,as the application programming interfaces(APIs) of SDN are low-level or functionality-restricted,SDN programmers cannot easily keep pace with the ever-changing devices,topologies,and demands of SDN.By deriving motivation from industry practice,we define a novel network algorithm programming language(NAPL) that enhances the SDN framework with a rapid programming flow from topology-based network models to C++ implementations,thus bridging the gap between the limited capability of existing SDN APIs and the reality of practical network management.In contrast to several state-of-the-art languages,NAPL provides a range of critical high-level network programming features:(1) topology-based network modeling and visualization;(2) fast abstraction and expansion of network devices and constraints;(3) a declarative paradigm for the fast design of forwarding policies;(4) a built-in library for complex algorithm implementation;(5) full compatibility with C++ programming;and(6) userfriendly debugging support when compiling NAPL into highly readable C++ codes.The expressiveness and performance of NAPL are demonstrated in various industrial scenarios originating from practical network management. | Jian WANG Jie AN Mingshuai CHEN Naijun ZHAN Lulin WANG Miaomiao ZHANG Ting GAN | 2020 | Science China(Information Sciences)2020，63，7： | 1 |
| 6 | Recent advances in program verification through computer algebra 显示文摘 | Yang Lu Zhou Chaochen Zhan Naijun | 2010 | Front Computer Science2010，4，1： | 1 |
| 7 | Symbolic decision procedure for termination of linear programs显示文摘 | Xia Bican Yang Lu Zhan Naijun | 2011 | Formal Aspects of Computing2011，23，2： | 1 |
| 8 | Learning real-time automata显示文摘Real-time automata(RTAs) are a subclass of timed automata with only one clock which resets at each transition. In this paper, we present an active learning algorithm for deterministic real-time automata(DRTAs) in both continuous-time semantics and discrete-time semantics. For a target language recognized by a DRTA A, we convert the problem of learning DRTA A to the problem of learning a canonical real-time automaton A with the same recognized language, i.e., L(A) = L(A). The algorithm is inspired by existing learning algorithms for symbolic automata. | Jie AN Lingtai WANG Bohua ZHAN Naijun ZHAN Miaomiao ZHANG | 2021 | Science China(Information Sciences)2021，64，9： | 0 |
| 9 | DISCOVERING NON-TERMINATING INPUTS FOR MULTI-PATH POLYNOMIAL PROGRAMS显示文摘This paper investigates the termination problems of multi-path polynomial programs(MPPs)with equational loop guards.To establish sufficient conditions for termination and nontermination simultaneously,the authors propose the notion of strong/weak non-termination which under/overapproximates non-termination.Based on polynomial ideal theory,the authors show that the set of all strong non-terminating inputs(SNTI) and weak non-terminating inputs(WNTI) both correspond to the real varieties of certain polynomial ideals.Furthermore,the authors prove that the variety of SNTI is computable,and under some sufficient conditions the variety of WNTI is also computable.Then by checking the computed SNTI and WNTI varieties in parallel,termination properties of a considered MPP can be asserted.As a consequence,the authors establish a new framework for termination analysis of MPPs. | LIU Jiang XU Ming ZHAN Naijun ZHAO Hengjun | 2014 | Journal of Systems Science & Complexity2014，27，6： | 0 |
| 10 | Safety guarantee for time-delay systems with disturbances显示文摘Time delays occur in various engineering applications because they may be inherent in the plants or caused by networks.In this paper,we investigate the safety verification problem of time-delay systems modeled by nonlinear delay differential equations subject to control inputs and disturbances in their dynamics.Building upon classical control barrier functionals,we develop the notions of input-to-state safety and input-to-state safe control barrier functionals,in which input-to-state safe control barrier functionals are used to guarantee the safety of time-delay systems with control inputs and disturbances.Three examples are provided to demonstrate the proposed approach. | Wenyou LIU Yunjun BAI Li JIAO Naijun ZHAN | 2023 | Science China(Information Sciences)2023，66，3： | 0 |
您所在的机构暂未开通此部分的功能，请联系管理员