检索结果-南通市图书馆

Verifying Time Petri Nets by linear Programming

在线全文

学校读者我要写书评

暂无评论

Journal of Computer Science & Technology 2001年第1期16卷 39-46页

作者：李宣东 State Key Laboratory of Novel Software Technology Department of Computer Science and Technology Nanjing University Nanjing P.R. China

The paper proposes an approach to solving some verification prob- lems of time Petri nets using linear programming. The approach is based on the observation that for loop-closed time Petri nets, it is only necessary to investigate a finite prefix of an untimed run of the underlying Petri net. Using the technique the paper gives solutions to reachability and bounded delay timing analysis problems. For both problems algorithms are given, that are decision procedures for loop-closed time Petri nets, and semi-decision procedures for general time Petri nets.

关键词： real-time system time Petri net linear programming model-checking

Empirically revisiting and enhancing automatic classification of bug and non-bug issues

在线全文

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2024年第5期18卷 25-44页

作者： Zhong li Minxue PAN Yu PEI Tian ZHANG linzhang WANG xuandong li State Key Laboratory for Novel Software Technology Nanjing UniversityNanjing 210023China Department of Computer Science and Technology Nanjing UniversityNanjing 210023China Software Institute Nanjing UniversityNanjing 210093China Department of Computing The Hong Kong Polytechnic UniversityHong KongChina

A large body of research effort has been dedicated to automated issue classification for Issue Tracking Systems(ITSs).Although the existing approaches have shown promising performance,the different design choices,including the different textual fields,feature representation methods and machine learning algorithms adopted by existing approaches,have not been comprehensively compared and *** fill this gap,we perform the first extensive study of automated issue classification on 9 state-of-the-art issue classification *** experimental results on the widely studied dataset reveal multiple practical guidelines for automated issue classification,including:(1)Training separate models for the issue titles and descriptions and then combining these two models tend to achieve better performance for issue classification;(2)Word embedding with Long Short-Term Memory(LSTM)can better extract features from the textual fields in the issues,and hence,lead to better issue classification models;(3)There exist certain terms in the textual fields that are helpful for building more discriminating classifiers between bug and non-bug issues;(4)The performance of the issue classification model is not sensitive to the choices of ML *** on our study outcomes,we further propose an advanced issue classification approach,DEEPLABEL,which can achieve better performance compared with the existing issue classification approaches.

关键词： issue tracking issue type prediction empirical study

Loop reduction techniques for reachability analysis of linear hybrid automata

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Science China(Information Sciences) 2012年第12期55卷 2663-2674页

作者： PAN MinXue,li You,BU Lei & li xuandong State Key Laboratory for Novel Software Technology,Department of Computer Science and Technology,Nanjing University,Nanjing 210093,China State Key Laboratory for Novel Software Technology Department of Computer Science and Technology Nanjing University Nanjing China

The problem of reachability analysis of linear hybrid automata(LHA) is very *** paper considers to improve the efficiency of the reachability analysis by optimizing the structures of *** identify two types of loops called the flexible loops and the zero loops,and present the techniques to replace the repetitions of those loops in the behavior of LHA with finite sequences of locations and in the meantime simplify the associated *** techniques work not only for the polyhedral computing based algorithms but also for the bounded model checkers.

关键词： real-time and hybrid systems linear hybrid automata reachability analysis

LDPChecker——一个实时和混成系统模型检验工具

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

计算机研究与发展 2005年第1期42卷 38-46页

作者：裴玉李宣东郑国梁南京大学计算机软件新技术国家重点实验室南京大学计算机科学与技术系南京 210093

混成系统是一类复杂系统,线性混成系统作为其重要子类,在形式方法中,人们通常使用线性混成自动机来对它建模.虽然线性混成自动机的模型检验问题总的来说还是不可判定的,但对于其中的正环闭合自动机,其对于线性时段性质的满足性能够通过... 详细信息

混成系统是一类复杂系统,线性混成系统作为其重要子类,在形式方法中,人们通常使用线性混成自动机来对它建模.虽然线性混成自动机的模型检验问题总的来说还是不可判定的,但对于其中的正环闭合自动机,其对于线性时段性质的满足性能够通过线性规划方法加以检验.为了实现自动检验正环闭合自动机对线性时段性质的满足性,设计并实现了工具LDPChecker.工具LDPChecker能够识别正环闭合自动机并对其进行相应的检验,其主要特色在于它能够对实时和混成系统检验包含可达性在内的许多实时性质,并且能够自动给出诊断信息.

关键词：实时和混成系统混成自动机线性时段性质模型检验

在线全文

学校读者我要写书评

暂无评论

隧道装配式预制仰拱结构选型研究

铁道建筑技术 2024年第8期 149-152,196页

作者：李煊栋中铁建安工程设计院有限公司陕西西安710086

对钻爆法隧道装配式预制仰拱结构选型设计进行研究。对比3类8种断面仰拱的力学性能,初步选择减重较多、力学性能较合理的3种断面并进行有限元分析。通过对整体模型和预制仰拱单块模型的对比研究,得出预制仰拱在施工机械荷载下的强度及... 详细信息

对钻爆法隧道装配式预制仰拱结构选型设计进行研究。对比3类8种断面仰拱的力学性能,初步选择减重较多、力学性能较合理的3种断面并进行有限元分析。通过对整体模型和预制仰拱单块模型的对比研究,得出预制仰拱在施工机械荷载下的强度及稳定性。结合计算结果提出最优断面型式,采用该断面型式的仰拱预制块相较于原设计,重量减少8.78 t,减少百分比43.9%,按承载力及正常使用极限状态设计均能满足要求。对其经济性进行分析对比,UHPC混凝土材料费用与原设计基本持平,当预制仰拱采用15 cm厚的UHPC板时,应力集中明显减少,塑性区域也较为合理和安全,可以作为预制仰拱的推荐型式。

关键词：装配式预制仰拱结构选型有限元分析 UHPC

UMLTGF:一个基于灰盒方法从UML活动图生成测试用例的工具

在线全文

学校读者我要写书评

暂无评论

计算机研究与发展 2006年第1期43卷 46-53页

作者：袁洁松王林章李宣东郑国梁南京大学计算机科学与技术系南京210093 南京大学软件新技术国家重点实验室南京210093

UML已经成为建模语言的事实标准,如何从UML分析设计模型生成测试用例也为面向对象软件测试带来了新的挑战·为了从UML设计模型中的活动图直接生成测试用例,给出了UML活动图的形式化定义和灰盒测试方法·该方法首先分析UML活动图上的所... 详细信息

UML已经成为建模语言的事实标准,如何从UML分析设计模型生成测试用例也为面向对象软件测试带来了新的挑战·为了从UML设计模型中的活动图直接生成测试用例,给出了UML活动图的形式化定义和灰盒测试方法·该方法首先分析UML活动图上的所有执行路径(每条路径称为一个测试场景),然后根据测试场景中的节点和转换所代表的活动及其输入/输出变量、相关约束条件等生成测试用例·并根据该方法实现了一个自动生成测试用例的工具UMLTGF,它可以从Rational Rose的规约文件中提取活动图信息并生成相应的测试用例·该工具能够提高软件测试的效率,降低测试成本·

关键词： UML 活动图灰盒方法测试场景测试用例

模板法合成三维菊花状TiO_2纳米花及其性能

在线全文

学校读者我要写书评

暂无评论

哈尔滨工业大学学报 2014年第2期46卷 55-60页

作者：李宣东付丽刘惠玲王炎文爱花刘臣娟哈尔滨工业大学理学院哈尔滨150001 哈尔滨工业大学市政环境工程学院哈尔滨150090 哈尔滨工业大学基础与交叉科学研究院哈尔滨150010

为了解决一维、二维纳米材料在降解有机污染物时,易发生团聚、催化活性低、难以回收利用等问题,以TiO2(P25)和NaOH为原料,ZnO为模板,采用水热法合成了三维菊花状TiO2纳米花.运用扫描电子显微镜、X射线衍射仪、氮气吸附脱附、紫外-可见... 详细信息

为了解决一维、二维纳米材料在降解有机污染物时,易发生团聚、催化活性低、难以回收利用等问题,以TiO2(P25)和NaOH为原料,ZnO为模板,采用水热法合成了三维菊花状TiO2纳米花.运用扫描电子显微镜、X射线衍射仪、氮气吸附脱附、紫外-可见漫反射、傅立叶红外等手段对合成的样品进行测试分析.结果表明:其花瓣是由TiO2纳米颗粒通过自组装定向排列而成的链状结构,构成纳米花的粒子晶粒尺寸约15 nm,花状结构尺寸约为5μm,结晶性良好,为锐钛矿相;比表面积为102.3 m2/g,平均孔径为17.41 nm;以亚甲基蓝为目标污染物,在紫外光照射下对其进行光催化性能实验,80 min亚甲基蓝的降解率为98%,催化活性高于P25,显示出较强的光催化活性.

关键词： TiO2 纳米花水热模板法自组装

在线全文

学校读者我要写书评

暂无评论

流动注射分析实验装置的研制

分析仪器 2000年第3期 24-26页

作者：尤宏姚杰李宣东余波哈尔滨工业大学化学实验中心哈尔滨150001

介绍了一种适用于教学应用的单通道流动注射分析仪。仪器采用夹管式电磁阀定时进样方法 ,结构简单 ,性能可靠。利用该仪器用反相流动注射分析法完成了电厂水中PO3- 4含量的测定。

关键词：流动注射分析单通道实验装置研制

在线全文

学校读者我要写书评

暂无评论

基于迁移系统分析的线性混成系统安全验证

计算机工程与应用 2013年第4期49卷 58-64,76页

作者：蒋慧卜磊李宣东南京大学计算机软件新技术国家重点实验室南京210046 南京大学计算机科学与技术系南京210046

混成自动机行为中既包含离散行为又包含连续行为,非常复杂。其安全性验证问题难以解决,即使是线性混成自动机,它的可达性问题也被证明是不可判定的。现有工具大都使用多面体计算来计算线性混成自动机的可达状态空间集,复杂度高,可处理... 详细信息

混成自动机行为中既包含离散行为又包含连续行为,非常复杂。其安全性验证问题难以解决,即使是线性混成自动机,它的可达性问题也被证明是不可判定的。现有工具大都使用多面体计算来计算线性混成自动机的可达状态空间集,复杂度高,可处理问题规模非常有限。为了避免这类问题,实现了一种新的工具。该工具将线性混成自动机表达为等价的迁移系统,并利用迁移系统上不变式生成相关工作对混成自动机进行验证。实验数据表明,方法有效可行,工具具有良好的性能。

关键词：线性混成自动机迁移系统安全性验证不变式生成