检索结果-南通市图书馆

Formal modelling of list based dynamic memory allocators

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Science China(Information Sciences) 2018年第12期61卷 81-96页

作者： Bin FANG Mihaela SIGHIREANU geguang pu Wen SU Jean-Raymond ABRIAL Mengfei YANG Lei QIAO Shanghai Key Laboratory of Trustworthy Computing East China Normal University IRIF University Paris Diderot and CNRS School of Computer Engineering and Science Shanghai University

Existing implementations of dynamic memory allocators(DMA) employ a large spectrum of policies and techniques. The formal specifications of these techniques are quite complicated in isolation and very complex when combined. Therefore, the formal reasoning on a specific DMA implementation is difficult for automatic tools and mostly single-use. This paper proposes a solution to this problem by providing formal models for a full class of DMA, the class using various kinds of lists to manage the memory blocks controlled by the DMA. To obtain reusable formal models and tractable formal reasoning, we organise these models in a hierarchy ranked by refinement relations. We prove the soundness of models and the refinement relations using the modeling framework Event-B and the theorem prover Rodin. We demonstrate that our hierarchy is a basis for an algorithm theory for list based DMA: it abstracts various existing implementations of DMA and leads to new DMA implementations. The applications of this formalisation include model-based code generation, testing, and static analysis.

关键词： dynamic memory allocators formal methods refinement Event-B Rodin model-based design

A novel requirement analysis approach for periodic control systems

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2013年第2期7卷 214-235页

作者： Zheng WANG geguang pu Jiangwen LI Yuxiang CHEN Yongxin ZHAO Mingsong CHEN Bin GU Mengfei YANG Jifeng HE Shanghai Key Laboratory of Trustworthy Computing Software Engineering Institute East China Normal UniversityChina Shanghai 200241 Beijing Institute of Control Engineering China Beijing 100080 School of Computing National University of SingaporeSingapore Singapore 119077 China Academy of Space Technology China Beijing 100094

Periodic control systems （PCSs） are widely used in real-time embedded system domain. However, traditional manual requirement analysis assumes the expert knowledge, which is laborious and error-prone. This paper proposes a novel requirement analysis approach, which supports the automated validation of the informal requirement specifi- cations. Based on the normalized initial requirement docu- ments, our approach can construct an intermediate SPARDL model with both formal syntax and semantics. To check the overall system behaviors, our approach can transform the SPARDL models into executable code for simulation. The derived prototype simulator from SPARDL models enables the testing-based system behavior validation. Moreover, our approach enables the analysis of the dataflow relations in SPARDL models. By revealing input/output and affecting re- lations, our dataflow analysis techniques can help software engineers to figure out the potential data dependencies be- tween SPARDL modules. This is very useful for the module reuse when a new version of the system is developed. A study of our approach using an industry design demonstrates the practicality and effectiveness of our approach.

关键词： SPARDL simulation dataflow analysis codegeneration

一种基于机器学习的模型检查算法性能预测方法

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

华东师范大学学报（自然科学版） 2024年第4期 18-29页

作者：张枨宇诸嘉逸黄怿豪杨迪李建文缪炜恺阎迪顾斌詹乃军蒲戈光苏黎世联邦理工学院计算机科学学院苏黎世8006 华东师范大学软件工程学院上海200062 南洋理工大学计算机科学与技术学院新加坡211106 中航商用航空发动机有限责任公司上海200241 中国航天科技集团有限公司北京100048 中国科学院软件研究所北京100190

与非图模型是一种表示电路设计的通用基础形式,同时也是模型检查器的一种通用输入格式.介绍了一种基于与非图结构编码的特征提取方法,并基于该方法实现了一种快速的组合模型检查器Liquid.所提出的结构编码的核心思想:首先罗列出与非图... 详细信息

与非图模型是一种表示电路设计的通用基础形式,同时也是模型检查器的一种通用输入格式.介绍了一种基于与非图结构编码的特征提取方法,并基于该方法实现了一种快速的组合模型检查器Liquid.所提出的结构编码的核心思想:首先罗列出与非图中所有可能的子结构,再将每个子结构出现的次数编码成向量,该向量即作为与非图的特征向量参与之后的机器学习过程.由于各种模型检查算法的性能在不同的与非图上参差不齐,Liquid的设计目标是组合多种模型检查算法,针对不同的与非图使用机器学习模型挑选出合适的算法.收集了目前所有的模型检查器基准测试集作为实验数据集并进行了实验.实验结果表明,Liquid在实验数据集上的表现优于所有组合中的独立模型检查算法,并有着不错的预测准确率.同时,还从多个维度分析了Liquid有效的原因.

关键词：模型检查与非图组合模型检查器

A Trade-off Design Approach for Integrating Cybersecurity,Safety and Other Aspects of Intelligent Connected Vehicles

维普期刊数据库

同方期刊数据库博看期刊评论

在线全文

学校读者我要写书评

暂无评论

A Trade-off Design Approach for Integrating Cybersecurity,Sa...

2022中国汽车工程学会年会暨展览会

作者： Yu Jinghua Luo Feng pu geguang Chen Mingsong Shanghai Trusted Industrial Control Platform Co. Ltd. East China Normal University Tongji University

With the increasing connectivity of the modern automotive,cybersecurity is becoming increasingly essential for an *** by design is a recommended way to protect automotive systems rather than after-sale ***,other than cybersecurity,an auto should also be safe and comfortable to transport people and *** to achieve a trade-off design considering various system requirements is a *** this paper,a trade-off design approach for integrating various aspects,like cybersecurity,safety,and user experience,is *** affecting map and the affecting score are proposed as tools to help the designer to select proper security countermeasures qualitatively or *** proposed methods are compatible with the international standard ISO/SAE21434.A case study of a Diagnostic on Internet Protocol(DoIP) system is demonstrated with details to show how to use the proposed methods,and also verify the feasibility and effectiveness of the approach.

关键词：

来源： cnki会议评论

在线全文

cnki会议

学校读者我要写书评

暂无评论

黑盒验证:无人驾驶系统安全挑战的解决途径

计算机研究与发展 2023年第7期60卷 1432-1432页

作者：蒲戈光华东师范大学软件工程学院上海200062

无人驾驶是未来交通的必然.当今,无人驾驶汽车在限制场景中已经展示出广泛的应用前景,如园区的物流配送、矿区的自动运载、固定路线的垃圾清除等.在无人驾驶的大规模应用之前,急需解决的挑战是无人驾驶的安全性.全球各国已经充分意识到... 详细信息

无人驾驶是未来交通的必然.当今,无人驾驶汽车在限制场景中已经展示出广泛的应用前景,如园区的物流配送、矿区的自动运载、固定路线的垃圾清除等.在无人驾驶的大规模应用之前,急需解决的挑战是无人驾驶的安全性.全球各国已经充分意识到了无人驾驶安全的重要性,不仅发布了多角度的无人驾驶安全技术标准,也出台了相关政策用以规范无人驾驶车辆的安全管理.黑盒验证是提高无人驾驶系统安全性的关键解决途径.黑盒验证是指无人驾驶的软硬件研发完成之后,对其系统进行测试确认,最大程度保证其系统安全性.

关键词：无人驾驶安全技术标准黑盒物流配送解决途径系统安全性安全挑战大规模应用

维普期刊数据库

The stochastic semantics and verification for periodic control systems

在线全文

学校读者我要写书评

暂无评论

Science China(Information Sciences) 2012年第12期55卷 2675-2693页

作者： YANG MengFei 3,WANG Zheng 1,2,pu geguang 1,Qin ShengChao 4,GU Bin 2 & HE JiFeng 1 1 Shanghai Key Laboratory of Trustworthy Computing,East China Normal University,Shanghai 200062,China 2 Beijing Institute of Control Engineering,Beijing 100190,China 3 China Academy of Space Technology,Beijing 100049,China 4 University of Teesside,TS1 3BA,UK 3. China Academy of Space Technology Beijing 100049 China1. Shanghai Key Laboratory of Trustworthy Computing East China Normal University Shanghai 200062 China2. Beijing Institute of Control Engineering Beijing 100190 China4. University of Teesside TS13BA Teesside UK

Periodic control systems(PCS) are widely used in the embedded industry like aerospace and *** systems usually run periodic tasks and respond to the external *** on our previous work on Mode diagram modeling(MDM) notations for specifying the periodic control system,we present the stochastic semantics for MDM in this *** stochastic semantics of MDM is based on the Markov *** semantics proposed here provides the basis for the satisfaction of formulae of the interval temporal logic(ITL) based specification language that is aimed to specify the properties of *** verify whether the system satisfies the ITL-based properties,we apply the statistical model checking technique to efficiently estimate the probability of the system satisfying the given property with a desired level of *** empirical experiments show that our approach is both effective and efficient.

关键词： periodic control system stochastic semantics statistical model checking