|
|
|
题名
|
作者
|
年代
|
出处
|
被引量
|
| 1 | Semantic theories of programs with nested interrupts显示文摘 | Yanhong HUANG Jifeng HE Huibiao ZHU Yongxin ZHAO Jianqi SHI Shengchao QIN | 2015 | Frontiers of Computer Science2015，9，3： | 1 |
| 2 | Timed automata patterns显示文摘 | DONG Jinsong HAO Ping QIN Shengchao | 2008 | IEEE Transactions on Software Engineering2008，2008，： | 1 |
| 3 | The stochastic semantics and verification for periodic control systems显示文摘Periodic control systems(PCS) are widely used in the embedded industry like aerospace and automotive.Such systems usually run periodic tasks and respond to the external signals.Based 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 paper.The stochastic semantics of MDM is based on the Markov chain.The 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 PCS.To 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 confidence.The empirical experiments show that our approach is both effective and efficient. | YANG MengFei WANG Zheng PU GeGuang Qin ShengChao GU Bin HE JiFeng | 2012 | Science China(Information Sciences)2012，55，12： | 0 |
| 4 | A New Species of the Genus Rhabdophis Fitzinger,1843(Squamata:Colubridae)in Southwestern Sichuan,China显示文摘The genus Rhabdophis is a group of widely distributed snakes with more than 20 species.Recent field surveys uncovered a species in southwestern China,which has long been considered as R.pentasupralabialis.Combined molecular and morphological analyses revealed it as a new species Rhabdophis chiwen sp.nov.Based on 12 specimens,this new species is distinguished by the following characters:1)dorsal body saddlebrown,dorsal scales typically with black margins forming spots and stripes,the margin of the outer row forming two faint dorsolateral black cross-bars alongside body;2)ventral scales 151–159,the outer margin of ventral scales and several lateral rows of dorsal scales forming ventrolateral longitudinal brownish-red coloration,with faint black spots in the middle of ventral scales;3)a black oblique stripe present below eyes,often with a black spot between the 2 nd and 3 rd supralabial and a black stripe on the 5 th supralabial;4)eyes dark khaki,pupils black;5)infralabials usually 7,the first four in contact with anterior chin-shields;6)temporal scales 1+1;7)dorsal scales in 15 rows,feebly keeled except the outer 1–2 rows;8)anal scale divided;subcaudals 45–59;9)preocular 1 and postoculars 3(occasionally 2);10)body medium-sized(snout-vent length:adult males 404–431 mm,adult females 409–476 mm);11)tail moderate(tail length/total length in adult males 0.205–0.238,in adult females0.172–0.193).With the discovery of this new species,the total number of species in genus Rhabdophis is 28 with 12 th species known to occur in China. | Yige PIAO Zening CHEN Yanqing WU Shengchao SHI Hirohiko TAKEUCHI Teppei JONO Masaya FUKUDA Akira MORI Yezhong TANG Qin CHEN Li DING | 2020 | Asian Herpetological Research2020，11，2： | 0 |
| 5 | Preface显示文摘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 section is to present state-of-the-art and high-quality original research in the area of software systems. | Tao Xie Shengchao Qin Wenhui Zhang | 2021 | Journal of Computer Science & Technology2021，36，6： | 0 |
| 6 | A Multi-Agent Spatial Logic for Scenario-Based Decision Modeling and Verification in Platoon Systems显示文摘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. | Jingwen Xu Yanhong Huang Jianqi Shi Shengchao Qin | 2021 | Journal of Computer Science & Technology2021，36，6： | 0 |
| 7 | Algorithms for checking channel passing in web service choreography显示文摘 | Hongli YANG Chao CAI Liyang PENG Xiangpeng ZHAO Zongyan QIU Shengchao QIN | 2013 | Frontiers of Computer Science2013，7，5： | 0 |
| 8 | BATON:symphony of random testing and concolic testing through machine learning and taint analysis显示文摘Random testing is scalable but often fails to hit corner program behaviors,while systematic testing(e.g.,concolic execution)is promising to cover corner program behaviors but is not scalable to explore all program behaviors.Prior attempts to integrate random testing with systematic testing lack targeted guidance.In this paper,we propose a guided hybrid testing approach,named BATon,to synergize random testing with concolic testing.It integrates the knowledge inside test cases and their executions into a conditional execution graph,and uses such knowledge to guide test case generation.Specifically,we learn classification models for some conditionals in the conditional execution graph in a demand-driven way.These models are used to guide random testing to reach and cover partially-covered conditionals.We further employ targeted concolic testing to cover conditionals that cannot be fully covered by guided random testing.We implemented BATon for Java and evaluated it on three benchmarks.The results show that BATon improved branch coverage and mutation score over random testing by 16.2%–29.4%and 19.0%–30.0%,over adaptive random testing by 16.8%–33.8%and 19.4%–34.2%,over concolic testing by 2.3%–29.9%and 2.9%–30.1%,and over simple hybrid testing by 1.6%–14.5%and 1.4%–18.7%. | Bihuan CHEN Yang LIU Xin PENG Yijian WU Shengchao QIN | 2023 | Science China(Information Sciences)2023，66，3： | 0 |
您所在的机构暂未开通此部分的功能，请联系管理员