检索结果-南通市图书馆

Generating Semi-Algebraic Invariants for Non-Autonomous Polynomial Hybrid Systems

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Journal of Systems Science & Complexity 2017年第1期30卷 234-252页

作者： WANG Qiuye LI Yangjia XIA Bican zhan naijun State Key Laboratory of Computer Science Institute of SoftwareChinese Academy of SciencesBeijing 100190China LMAM&School of Mathematical Sciences Peking UnivcrsityBeijing 100871China

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.

关键词： Hybrid systems invariants non-a utonomous systems polynomial ideals semi-algebraic sets.

Safety guarantee for time-delay systems with disturbances

在线全文

学校读者我要写书评

暂无评论

Science China(Information Sciences) 2023年第3期66卷 118-132页

作者： Wenyou LIU Yunjun BAI Li JIAO naijun zhan State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences University of Chinese Academy of Sciences

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.

关键词： time-delay systems delay differential equations control barrier functionals controllers safety

DISCOVERING NON-TERMINATING INPUTS FOR MULTI-PATH POLYNOMIAL PROGRAMS

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Journal of Systems Science & Complexity 2014年第6期27卷 1286-1304页

作者： LIU Jiang XU Ming zhan naijun ZHAO Hengjun Chongqing Key Laboratory of Automated Reasoning and Cognition CIGITChinese Academy of Sciences Department of Computer Science and Technology East China Normal University State Key Laboratory of Computer Science Institute of SoftwareChinese Academy of Sciences

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/over- approximates 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 tile 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 consid- ered MPP can be asserted. As a consequence, the authors establish a new framework for termination analysis of MPPs.

关键词： Polynomial ideals polynomial programs termination analysis.

From model to implementation: a network algorithm programming language

在线全文

学校读者我要写书评

暂无评论

Science China(Information Sciences) 2020年第7期63卷 205-221页

作者： Jian WANG Jie AN Mingshuai CHEN naijun zhan Lulin WANG Miaomiao zhanG Ting GAN State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences University of Chinese Academy of Sciences School of Software Engineering Tongji University Network Integration Technology Research Department Huawei Technologies Co. Ltd. School of Computer Science Wuhan University

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.

关键词： software-defined networking(SDN) network algorithm programming language(NAPL) network abstraction

Behavior modeling and verification of movement authority scenario of Chinese Train Control System using AADL

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Science China(Information Sciences) 2015年第11期58卷 125-144页

作者： AHMAD Ehsan DONG YunWei LARSON Brian Lü JiDong TANG Tao zhan naijun School of Computer Science Northwestern Polytechnical University State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences Computing and Information Systems Kansas State University State Key Laboratory of Rail Traffic Control and Safety Beijing Jiaotong University

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 *** 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 *** 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.

关键词： AADL behavior modeling BLESS annex CTCS hybrid annex train control system

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

时延混成系统的切换控制器合成

中国科学：数学 2021年第1期51卷 97-114页

作者：白云军甘庭焦莉薛白詹乃军中国科学院大学中国科学院软件研究所计算机科学国家重点实验室北京100190 武汉大学计算机学院武汉430072

如何设计安全、可靠的信息物理融合系统是计算机科学和控制理论面临的一个重大挑战.时延现象在信息物理融合系统中普遍存在,时延对系统的稳定性、安全性和控制性能具有实质性影响.但是在已有时延系统验证和控制器合成的工作中往往忽略... 详细信息

如何设计安全、可靠的信息物理融合系统是计算机科学和控制理论面临的一个重大挑战.时延现象在信息物理融合系统中普遍存在,时延对系统的稳定性、安全性和控制性能具有实质性影响.但是在已有时延系统验证和控制器合成的工作中往往忽略时延因素,这会导致在不考虑时延情况下能保证稳定和安全的系统在实际运行时因为时延原因而不再稳定和安全.因为时延使得系统的行为演化不仅与当前状态有关,还依赖于系统的历史状态,所以时延混成系统的验证和控制合成更加困难.本文研究信息物理融合系统在考虑时延情形下切换控制器合成问题,提出基于不变式生成技术的控制器合成方法.首先,利用谱分析和线性化技术将时延系统的微分不变式生成问题归结为有界时间的可达集计算问题;然后,提出基于抽象精化的算法计算时延系统有界时间可达集的上近似;最后,实现本文算法并使用实例验证该方法的有效性.

关键词：时延混成系统时延微分方程微分不变式切换控制器安全性

在线全文

学校读者我要写书评

暂无评论

复杂系统规约、分析与验证发展现状与展望

前瞻科技 2023年第1期2卷 7-22页

作者：詹乃军王戟中国科学院软件研究所天基综合信息系统重点实验室中国科学院软件研究所计算机科学国家重点实验室国防科技大学计算机学院国防科技大学高性能计算国家重点实验室

形式化方法包括计算系统（软硬件和网络）的规约、构造、分析与验证的数学基础、技术和工具。随着安全攸关系统在国民经济和国防等关键领域的应用越来越多，复杂系统可信性问题日益凸显。形式化方法已经成为开发安全可靠的安全攸关系统... 详细信息

形式化方法包括计算系统（软硬件和网络）的规约、构造、分析与验证的数学基础、技术和工具。随着安全攸关系统在国民经济和国防等关键领域的应用越来越多，复杂系统可信性问题日益凸显。形式化方法已经成为开发安全可靠的安全攸关系统的关键技术之一，也是解决中国“缺芯少魂”的核心技术之一，同时也是国际学术前沿。文章回顾国内外形式化方法研究现状，分析国内外研究差距，并提出加强中国这方面基础研发的若干建议。

关键词：形式化方法安全攸关系统形式规约形式分析与验证

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

中国高速铁路列控系统的形式化分析与验证

中国科学：信息科学 2015年第3期45卷 417-438页

作者：郭丹青吕继东王淑灵唐涛詹乃军周达天邹亮中国科学院软件研究所计算机科学国家重点实验室北京100190 北京交通大学轨道交通运行控制国家工程中心北京100190 北京交通大学轨道交通控制与安全国家重点实验室北京100190

高速铁路列控系统的安全与否直接涉及人民的生命财产安全,对高速铁路列控系统进行严格的形式化验证具有重要意义.但是随着高速铁路列控系统软件以及硬件规模的不断增大,系统的复杂性有了很大的提高,直接对高速铁路列控系统进行形式化验... 详细信息

高速铁路列控系统的安全与否直接涉及人民的生命财产安全,对高速铁路列控系统进行严格的形式化验证具有重要意义.但是随着高速铁路列控系统软件以及硬件规模的不断增大,系统的复杂性有了很大的提高,直接对高速铁路列控系统进行形式化验证已经变得越来越困难.另一方面,由于图形化建模和仿真表现方式直观且易于理解,在工程实践中已经得到了广泛的应用.因此,为了更好地保证铁路系统的安全,对系统进行仿真,排除部分安全隐患显得尤为重要.本文通过使用Simulink/Stateflow建模工具对高速铁路列控系统的行车许可,等级升级及部分模式转换场景进行了建模.该模型具有普适性,通过修改参数信息,可以对不同的等级转换和模式转换的组合情况进行仿真.本文使用该模型对10种组合情况进行了仿真,发现在某些情况下可能会出现不正常停车或者等级转换失败的现象.类似于测试,仿真仅仅能够发现错误,如未发现错误,也不能证明系统是正确的.因为仿真的这种不完备性,对仿真辅助形式验证在安全攸关系统设计中非常必要.为此,取其中一个不正常停车的场景进行了形式验证,验证结果证明在任何情况下都不能正常停车.

关键词：中国高速铁路列控系统 Simulink/Stateflow 仿真模式转换等级转换形式化验证

迎接人机物融合泛在计算时代,提升关键软件技术创新与供给能力

在线全文

学校读者我要写书评

暂无评论

前瞻科技 2023年第1期2卷 5-6页

作者：李宣东王戟詹乃军南京大学国防科技大学中国科学院软件研究所

1人机物融合泛在计算打开了应用需求的新空间近10年来,云计算、物联网、大数据、人工智能等信息领域技术浪潮风起云涌,推动信息世界、物理世界和人类社会日趋交叉融合,正在逐渐形成万物互联、人机交互、天地一体的泛在计算环境,从而催... 详细信息

1人机物融合泛在计算打开了应用需求的新空间近10年来,云计算、物联网、大数据、人工智能等信息领域技术浪潮风起云涌,推动信息世界、物理世界和人类社会日趋交叉融合,正在逐渐形成万物互联、人机交互、天地一体的泛在计算环境,从而催生人机物融合应用场景不断涌现。一方面,包括汽车、建筑、车间、企业、社区、园区、城市等在内的人机物融合应用场景孕育出一批人机物融合应用需求;另一方面,这些人机物融合应用场景还各自汇聚了一批泛在软硬件异构资源系统,包括计算、网络、感知、数据、服务系统等,正如中国科学院院士吕建所说“应用场景就是计算机”。

关键词：泛在计算人机物融合人工智能中国科学院院士云计算大数据人机交互物联网