检索结果-南通市图书馆

A Multi-Agent Spatial Logic for Scenario-Based Decision Modeling and Verification in Platoon Systems

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Journal of Computer Science & Technology 2021年第6期36卷 1231-1247页

作者： Jingwen Xu Yanhong Huang Jianqi Shi shengchao qin National Trusted Embedded Software Engineering Technology Research Center East China Normal University Shanghai 200062China College of Computer Science and Software Engineering Shenzhen UniversityShenzhen 518061China

To cater for the scenario of coordinated transportation of multiple trucks on the highway,a platoon system for autonomous driving has been extensively explored in the industry.Before such a platoon is deployed,it is necessary to ensure the safety of its driving behavior,whereby each vehicle’s behavior is commanded by the decision-making function whose decision is based on the observed driving scenario.However,there is currently a lack of verification methods to ensure the reliability of the scenario-based decision-making process in the platoon system.In this paper,we focus on the platoon driving scenario,whereby the platoon is composed of intelligent heavy trucks driving on cross-sea highways.We propose a formal modeling and verification approach to provide safety assurance for platoon vehicles’cooperative driving behaviors.The existing Multi-Lane Spatial Logic(MLSL)with a dedicated abstract model can express driving scene spatial properties and prove the safety of multi-lane traffic maneuvers under the single-vehicle perspective.To cater for the platoon system’s multi-vehicle perspective,we modify the existing abstract model and propose a Multi-Agent Spatial Logic(MASL)that extends MLSL by relative orientation and multi-agent observation.We then utilize a timed automata type supporting MASL formulas to model vehicles’decision controllers for platoon driving.Taking the behavior of a human-driven vehicle(HDV)joining the platoon as a case study,we have implemented the model and verified safety properties on the UPPAAL tool to illustrate the viability of our framework.

关键词： autonomous driving decision-making model platoon system safety verification timed automaton

Semantic theories of programs with nested interrupts

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2015年第3期9卷 331-345页

作者： Yanhong HUANG Jifeng HE Huibiao ZHU Yongxin ZHAO Jianqi SHI shengchao qin National Trusted Embedded Software Engineering Technology Research Center East China Normal University Shanghai 200062 China Shanghai Key Laboratory of Trustworthy Computing East China Normal University Shanghai 200062 China School of Computer Science and Software Engineering Shenzhen University Shenzhen 518060 China

In the design of dependable software for embed- ded and real-time operating systems, time analysis is a cru- cial but extremely difficult issue, the challenge of which is exacerbated due to the randomness and nondeterminism of interrupt handling behaviors. Thus research into a theory that integrates interrupt behaviors and time analysis seems to be important and challenging. In this paper, we present a pro- gramming language to describe programs with interrupts that is comprised of two essential parts： main program and inter- rupt handling programs. We also explore a timed operational semantics and a denotational semantics to specify the mean- ings of our language. Furthermore, a strategy of deriving de- notational semantics from the timed operational semantics is provided to demonstrate the soundness of our operational se- mantics by showing the consistency between the derived de- notational semantics and the original denotational semantics.

关键词： embedded and real-time operating systems in-terrupts operational semantics denotational semantics semantics linking

Algorithms for checking channel passing in web service choreography

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2013年第5期7卷 710-728页

作者： Hongli YANG Chao CAI Liyang PENG Xiangpeng ZHAO Zongyan QIU shengchao qin College of Computer Sciences Beijing University of Technology Beijing 100222 China Institute of Software Chinese Academy of Sciences Beijing 100080 China China Defense Science and Technology Information Center Beijing 100142 China Vancl Research Lab Beijing 100124 China Facebook Inc. California 94025 USA LMAM and Department of Informatics School of Mathematical Sciences Peking University Beijing 100871 China School of Computing University of Teesside MiddlesbroughTS 1 3BA UK

Web service choreography describes global mod- els of service interactions among a set of participants. For an interaction to be executed, the participants must know the required channel（s） used in the interaction, otherwise the ex- ecution will get stuck. Since channels are composed dynami- cally, the initial channel set of each participant is often insuf- ficient to meet the requirements. It is the responsibility of the participants to pass required channels owned （known） by one to others. Since service choreography may involve many par- ticipants and complex channel constraints, it is hard for de- signers to specify channel passing in a choreography exactly as required. We address the problem of checking whether a service choreography lacks channels or has redundant chan- nels, and how to automatically generate channel passing based on interaction flows of the service choreography in the case of channel absence. Concretely, we propose a sim- ple language Chorc, a channel interaction sub-language for modeling the channel passing aspect of service choreography. Based on the formal operational semantics of Chore, the algo- rithms for static checking of service choreography and gen- erating channel passing are also studied, and the complexity results of algorithms are discussed. Moreover, some illus- trated service choreography examples are presented to show how to formalize and analyze service choreography with channel passing in Chorc.

关键词： web service choreography channel passing al- gorithms

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Preface

Journal of Computer Science & Technology 2021年第6期36卷 1229-1230页

作者： Tao Xie shengchao qin Wenhui Zhang School of Computer Science Peking UniversityBeijing Senior Software Expert Huawei Hong Kong Research CentreHong Kong Institute of Software Chinese Academy of SciencesBeijing

As a continuation of previous years1 special section on software systems,this special section encourages and promotes research to address challenges from the perspective of software systems.The goal of this special se... 详细信息

关键词： systems. continuation section

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Preface

Journal of Computer Science & Technology 2022年第1期37卷 1-3页

作者：谢涛秦胜潮张文辉孙军卜磊李戈 School of Computer Science Peking UniversityBeijing Huawei Hong Kong Research Centre Hong KongChina Institute of Software Chinese Academy of SciencesBeijing Singapore Management University Singapore Department of Computer Science and Technology&State Key Laboratory for Novel Software Technology Nanjing UniversityNanjing

As a continuation of previous years’special section on software systems,this special section encourages and promotes research to address challenges from the perspective of software systems.The goal of this special section is to present state-of-the-art and high-quality original research in the area of software systems.This special section is split in two parts,with the first part published earlier in the last issue in November 2021 and the second part published in this current issue.

关键词： systems. continuation section

四川省阿坝州碘缺乏病＂十二五＂终期考核评估结果分析

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

中华地方病学杂志 2018年第6期37卷 477-480页

作者：秦胜超张霞四川省阿坝州疾病预防控制中心地病所马尔康624000

目的评价四川省阿坝州碘缺乏病实现控制和消除目标进展，根据评价结果，确定碘缺乏病分类防控策略，实施防控工作精细化。方法根据《四川省地方病防治“十二五”规划终期考核评估方案》要求，2015年3 - 6月在阿坝州13个县（市），开... 详细信息

目的评价四川省阿坝州碘缺乏病实现控制和消除目标进展，根据评价结果，确定碘缺乏病分类防控策略，实施防控工作精细化。方法根据《四川省地方病防治“十二五”规划终期考核评估方案》要求，2015年3 - 6月在阿坝州13个县（市），开展终期考核评估，进行管理指标评分。每个县（市）按东、西、南、北、中5个方位各抽取1个乡（镇），每个乡（镇）抽取4个行政村，每个行政村抽检15户居民家中食盐样品，采用仲裁法（GB／T 13025.7-1999）检测盐碘含量。在所抽取的乡（镇）各抽取1 所村小学，每所小学抽取40名8 - 10岁儿童（男、女各半）尿样，采用砷铈催化分光光度法（WS／T 107-2006）检测尿碘含量；并用触诊法检查儿童甲状腺肿大情况。在所抽取的乡（镇）各抽取20名孕妇的尿样，检测尿碘含量；同时，在每个乡（镇）开展尿碘含量检测的孕妇中，各抽取10人进行问卷调查，了解孕妇健康教育知识知晓情况。结果阿坝州县级管理指标平均分为92分。共抽取居民盐样3 941份，盐碘中位数为28.8 mg／kg，合格碘盐食用率为96.6%（3 806／3 941），碘盐覆盖率为99.6%（3 927／3 941 ）。共检测儿童尿样2 866份，尿碘中位数为160.0 μg／L，尿碘〈 50 μg／L的占4.6%（131／2 866）；共检查儿童甲状腺2 819 人，甲状腺肿大率为0.7%（19／2 819）。共检测孕妇尿样1 143份，尿碘中位数为188.3 μg／L，尿碘〈 150 μg／L的占27.9%（ 319／1 143）；共收集调查问卷650份，孕妇健康教育知识知晓率为78.3%（1 527／1 950）。结论阿坝州持续保持消除碘缺乏病状态，人群碘营养状况较好，但需进一步加强碘盐市场监管和健康教育工作。

关键词：儿童孕妇甲状腺碘盐类尿考核评估

基于SOA与虚拟私有云的断路器状态可视化监测系统

在线全文

学校读者我要写书评

暂无评论

电力系统保护与控制 2020年第17期48卷 155-161页

作者：练椿杰韦化覃圣超李宗声广西电力系统最优化与节能重点实验室(广西大学) 广西南宁530004

提出了基于面向服务架构(Service-Oriented Architecture,SOA)及虚拟私有云(Virtual Private Cloud,VPC)的断路器状态实时可视化监测系统,解决了现有SCADA系统在大数据背景下断路器信息分散不集中、可视化困难的问题。系统采用SOA架构,... 详细信息

提出了基于面向服务架构(Service-Oriented Architecture,SOA)及虚拟私有云(Virtual Private Cloud,VPC)的断路器状态实时可视化监测系统,解决了现有SCADA系统在大数据背景下断路器信息分散不集中、可视化困难的问题。系统采用SOA架构,将各基础功能封装成接口服务,相互调用以实现整体功能,具备低耦合、易维护、易拓展的特点。将系统部署至虚拟私有云,整合虚拟私有云高性能、低成本、强灾备、高安全性的优势,实现了可交互、可跨平台的B/S模式的Web客户端。其作为一个决策支持系统,为电网工作人员可靠地监控整个电网提供了强有力的依据。对所提系统的原理、结构、特点及部署过程进行了详细地介绍。运行结果表明,该系统提高了电力系统的安全稳定特性,满足电网的可靠性要求,且应用于实际电力系统,具有良好的应用前景。

关键词： SOA 虚拟私有云断路器状态监测可视化安全稳定

Karyotypes of three species of the marine Veneroida molluscs

在线全文

学校读者我要写书评

暂无评论

Acta Oceanologica Sinica 2003年第4期22卷 671-678页

作者： Sun Zhenxing1, Shao Yanqun1, Guo shengchao1, qin Yan1, Yang Aiguo2 1. Department of Biological Science and Biotechnology, Yantai Normal University, Yantai 264025, China. 2. Yellow Sea Fisheries Research Institute, qingdao 266071, China. Dept. of Biol. Sci./Biotechnology Yantai Normal University Yantai 264025 China Yellow Sea Fisheries Research Inst. Qingdao 266071 China

The karyotypes of three species of marine Veneroida molluscs, Solen grandis Dunker, Saxidomus purpuratus Sowerby and Mactra chinensis Philippi were studied by using the adult gill tissues. The chromosomes were-prepared through injecting phytohemagglutinin (PHA) and colchicine, hypotonic treatment, chopping air-dry, and squashing technology. The results show that the diploid chromosome numbers of the three Veneroida species are the same as 2n = 38. The karyotype of Solen grandis is 26m + 6sm + 2st + 4t, NF = 70, the karyotype of Saxidomus purpuratus is 32m + 2sm + 4st/t, NF = 72, and the karyotype of Mactra chinensis is 20m + 16sm + 2st/t, NF = 74. Satellite and sex chromosome were not found among the chromosomes of three species.

关键词： Solen grandis Dunker Saxidomus purpuratus Sowerby Mactra chinensis Philippi chromosome karyotype

四川省阿坝州大骨节病患者患病及生活现状调查

在线全文

学校读者我要写书评

暂无评论

中华地方病学杂志 2016年第7期35卷 502-507页

作者：刘玲马文军秦胜超明迪尧中国疾病预防控制中心环境与健康相关产品安全所北京100050 北京大学医学部公共卫生学院劳动卫生与环境卫生学系北京100050 四川省阿坝州疾病预防控制中心地方病防治研究所阿坝州624000

目的了解阿坝州大骨节病患者疾病状况、生活现状及大骨节病防治措施实施情况。方法2009—2011年采用分层整群抽样方法，抽取阿坝州大骨节病病区村共26个，临近非病区村12个，使用自行设计的访谈问卷入户调查病区村大骨节病患者1347名及... 详细信息

目的了解阿坝州大骨节病患者疾病状况、生活现状及大骨节病防治措施实施情况。方法2009—2011年采用分层整群抽样方法，抽取阿坝州大骨节病病区村共26个，临近非病区村12个，使用自行设计的访谈问卷入户调查病区村大骨节病患者1347名及非病区村常住居民447名作为对照。调查内容包括：①调查对象一般人口学特征，如姓名、性别、年龄、受教育程度、家庭年收入、婚姻状况等；②大骨节病患者患病相关的基本信息，包括确诊时间、地点、治疗情况、是否拍手部X光片、是否同时患有氟斑牙、氟骨症等：③调查对象的基本生活习惯，如饮水、主食来源、主食类型、粮食存放地点、喝茶习惯等。结果共522名（38．8％，522／1347）大骨节病患者和12名（2．7％，12／447）对照人群确定其父母有大骨节病。绝大部分大骨节病患者（99．0％，1334／1347）是2—5年内在县疾病预防控制中心或县一级医院确诊，确诊后有97．6％（1314／1347）的患者通过服用止痛片、亚硒酸钠、维生素E进行治疗。大骨节病患者同时患氟斑牙和氟骨症的检出率分别为66．3％（893／1347）、59．9％（807／1347），阿坝州大骨节病患者和对照人群2004年以前主要饮用河水．主食来源是当地自产粮食（96．7％，1716／1774），以青稞、玉米等为主（93．5％，1660／1775）；2004年至今水源都改为自来水，主食来源主要是两种粮食混用或者商品粮为主（96．9％，1727／1783），主食类型以大米和面粉为主（98．4％，I765／1794）。94．1％（1267／1347）大骨节病患者有喝茶的习惯。结论有关改水、改粮措施在阿坝地区实施较好，建议进一步采取以家庭为单位进行重点家庭宣传和防治、加强当地医疗保障体系及针对性的治疗等方式来改善当地大骨节病患者的整体患病状况及生活质量。

关键词：大骨节病现况调查疾病状况生活现状