检索结果-内蒙古大学图书馆

Theoretical Aspects of software engineering (TASE)

作者： Kangli He Min Zhang Jia He Yixiang Chen MoE Engineering Research Center for Software/Hardware Co-design Technology and Application Shanghai Key Laboratory of Trustworthy Computing East China Normal University Shanghai China

ISBN: (纸本)9781467376136

Pipe protocol, proposed by Zhao [1] in early 2013, is one application layer protocol and one way to establish the Internet of Things, under which can different kinds of hardware platforms communicate with each other faster and more safely. As an upper layer protocol, Pipe protocol doesn't define details, but during the implementation, probabilistic and nondeterministic behaviors, such as data loss and external choice, are possible to happen. In this paper, we use probabilistic model checker, PRISM, to construct the probabilistic Pipe protocol as Probabilistic Timed Automata (PTAs), then verify some useful time-bounded properties, written in Probabilistic computation Tree Logic (PCTL), like, “Maximum probability that the pipe is shut down after Source node sends all 5 data packets within 50 μs”. The results show that the data loss probabilities, number of data and deadline should be restricted suitably if we require the maximum probability of the goal reaches some value. Our model is proved to be meaningful and we can give helpful suggestions to improve the implementation of Pipe protocol.

关键词： Probabilistic logic Protocols Clocks Automata Real-time systems computational modeling Model checking

来源：评论

学校读者我要写书评

暂无评论

Parallel implementation of dense optical flow computation on many-core processor 1

引用

15th International conference on Algorithms and Architectures for Parallel Processing, ICA3PP 2015

作者： Chen, Wenjie Yu, Jin Zhang, Weihua Jiang, Linhua Zhang, Guanhua Chai, Zhilei MoE Engineering Research Center for Software/Hardware Co-design Technology and Application East China Normal University Shanghai200061 China School of IoT Engineering Jiangnan University Wuxi214122 China Parallel Processing Institute Fudan University Shanghai200433 China Shanghai Key Lab of Modern Optical Systems University of Shanghai for Science and Technology Shanghai200093 China

ISBN: (数字)9783319271194

ISBN: (纸本)9783319271187

computation of optical flow is a fundamental step in computer vision applications. However, due to its high complexity, it is difficult to compute a high-accuracy optical flow field in real time. This paper proposes a parallel computing approach for fast computation of high-accuracy optical flow field. It is specially designed for Tilera, a typical many-core processor with 36 tiles. By efficiently exploiting the advantages of the mesh architecture of Tilera, and by appropriately handling the parallelism inherent in the optical flow computation, the proposed implemention is able to significantly reduce the computation time while keep a low power consumption. Experiment shows that, for a 640×480 image, the computation time is only 0. 80 seconds per frame. It is 2. 56 times faster than on a typical CPU i3-3240 (3. 4GHz), and the power consumption as less as 1/6. Experimental results also show that the proposed parallel approach is highly scalable for variable requirements on computation speeds and power consumptions, since it can flexibly selects a proper number of computing cores. © Springer International Publishing Switzerland 2015.

关键词： Parallel processing systems

来源：评论

学校读者我要写书评

暂无评论

Modeling and Verification of Space-Air-Ground Integrated Networks on Requirement Level Using STeC

Modeling and Verification of Space-Air-Ground Integrated Net...

引用

Theoretical Aspects of software engineering (TASE)

作者： Zhihua Yang Bo Xiao Yixiang Chen Institute of Software Engineering East China Normal University Shanghai China MoE Engineering Research Center for Software/Hardware Co-design Technology and Application East China Normal University Shanghai China

ISBN: (纸本)9781467376136

This paper introduces a domain Spatio-Temporal consistency (STeC) language for the application domain of space-air-ground integrated networks. The STeC language is taken as the foundation of modeling our systems, bacause it works well on specifying real-time systems concerning not only the time characteristic but also the location characteristic and the consistency between them. In this paper, a domain-STeC language is devised and applied to model satellite observation processes. We use two tools to check and verify this STeC model, the syntax and spatio-temporal consistency were checked in STeC tool, and after being transformed into timed automata model, some further verification can be finished in UPPAAL tool. It shows that the instantiated STeC approach is suitable for modeling and verifying space-air-ground integrated networks on the requirement level. This work helps to ensure the spatial-temporal consistency in that application domain, and increases the reliability and dependability of our system.

关键词： Satellites Automata Real-time systems Earth Clocks software Reliability

来源：评论

学校读者我要写书评

暂无评论

complexity Measure Based on ProgramSlicing and Its Validation

引用

Wuhan University Journal of Natural Sciences 2014年第6期19卷 512-518页

作者： TAO Hongwei CHEN Yixiang School of Computer and Communication Engineering Zhengzhou University of Light Industry MoE Engineering Research Center for Software/Hardware Co-design Technology and Application East China Normal University

The popular single-factor complexity measure cannot comprehensively reflect program complexity and the existing hybrid complexity measure cannot express the interactive behaviors of programs. To treat these problems, in this paper, we propose a complexity measure based on program slicing（CMBPS）. CMPBS not only can evaluate factors which affect program complexity such as the length of the program, control flow, data flow and data types of output variables, but also can give expression of the interactive relation between programs. And we also prove that CMBPS satisfies all of Weyuker properties. compared with the popular complexity measures, CMBPS is a well-structured complexity measure.

关键词： program slicing complexity measure Weyuker properties validation

来源：评论

学校读者我要写书评

暂无评论

confidential Parcel Delivery System

Confidential Parcel Delivery System

引用

2014 Asia——Pacific Management and engineering conference(APME 2014)

作者： WENJIE CHEN GUANHUA ZHANG MoE Engineering Research Center for Software/Hardware Co-design Technology and Application East China Normal University

The current express parcel delivery systems have a big drawback that the private information of the recipient and the sender cannot be protected *** paper proposes a novel system to keep the *** of an explicit waybill,this system uses a well coded logistics label to assure that only necessary part ofinformation is exposed to the related staff during the entire delivery *** system also has additional advantages such as verifying e-trade facticity,avoiding disputation on signature and preventing malicious *** system is also good for "the order oriented production".

关键词： confidential Parcel Delivery System

来源：评论

学校读者我要写书评

暂无评论

coalgebras for fuzzy transition systems

Coalgebras for fuzzy transition systems

引用

作者： Wu, Hengyang Chen, Yixiang Information Engineer College Hangzhou Dianzi University Hangzhou 310018 China MoE Engineering Research Center for Software/Hardware Co-design Technology and Application Shanghai Key Lab for Trustworthy Computing East China Normal University Shanghai 200062 China

This paper studies a coalgebraic theory of fuzzy transition systems. Main conclusions include: the functor FA for deterministic fuzzy transition systems and the functor (Pa°F)A for nondeterministic fuzzy transition systems preserve weak pullbacks, and the functor FA has a final coalgebra under some restricted conditions. Moreover, we show how to get a concrete (fuzzy) bisimulation from a coalgebraic bisimulation. Crown copyright © 2014 Published by Elsevier B.V. All rights reserved.

关键词： Algebra

来源：评论

学校读者我要写书评

暂无评论

A Hybrid Clock System Related to STeC Language

A Hybrid Clock System Related to STeC Language

引用

International conference on Secure software Integration and Reliability Improvement companion (SSIRI-C)

作者： Yixinag Chen Yuanrui Zhang MoE Engineering Research Center for Software/Hardware Co-design Technology and Application East China Normal University Shanghai China University of Nice Sophia Antipolis Nice France Software Engineering Institute East China Normal University Shanghai China

Cyber-Physical Systems(CPS) is a new trend of real-time systems in the area of distributed embedded systems or networked agent systems. The first author introduced a specification language for real-time system, called as spatial-temporal consistency language (Shortly, STeC) in 2010. In this paper, the authors introduce a novel clock system, called as hybrid clock, to specify both logical and chronometric time aspect of real time system. Some operations on hybrid clocks and relations between hybrid clocks are introduced. A satisfaction relation between a hybrid clock and a STeC design of real time system specified in term with STeC language is defined. Some properties and CPS case studies are given in this paper.

关键词： Clocks Real-time systems Integrated circuits Indexes Sensors Schedules

来源：评论

学校读者我要写书评

暂无评论

Timed Automata Semantics of Spatial-Temporal consistency Language STeC

Timed Automata Semantics of Spatial-Temporal Consistency Lan...

引用

Theoretical Aspects of software engineering (TASE)

作者： Yuanrui Zhang Frederic Mallet Yixiang Chen Polytech Nice Sophia University Nice Sophia Antipolis Nice France Institute of Software Engineering East China Normal University Shanghai China Univ. Nice Sophia Antipolis CNRS Sophia Antipolis France MoE Engineering Research Center for Software/Hardware Co-design Technology and Application East China Normal University Shanghai China

Intelligent Transportation Systems (ITS) are a class of quickly evolving modern safety-critical embedded systems. Dealing with their growing complexity demands a high-level formal modeling language along with adequate verification techniques. STeC has recently been introduced as a process algebra that deals natively with both spatial and temporal properties. Even though STeC has the right expressive power, it does not provide a direct tooled support for verification. We propose to encode STeC specifications as Timed Automata to provide such a support and we illustrate our transformation strategy on a simple example.

关键词： Clocks Automata Semantics Syntactics Labeling Unified modeling language Educational institutions

来源：评论

学校读者我要写书评

暂无评论

An improved light-weight trust model in WSN

引用

computer Modelling and New Technologies 2014年第4期18卷 57-61页

作者： Wang, Na Pang, Yanxia MoE Engineering Center for Software/Hardware Co-design Technology and its Application East China Normal University No.3663 North Zhongshan Rd Shanghai 200062 China School of Computer and information Shanghai Second Polytechnic University No. 2360 Jinhai Rd Shanghai 201209 China

WSN is often deployed in unattended or even hostile environments. Therefore, providing security in WSN is a major requirement for acceptance and deployment of WSN. Furthermore, establishing trust in a clustered environment can provide numerous advantages. We proposed a light-weight trust model which considers data aggregation and communication failure due to wireless channels. It computes retransmission rate to get success, failed and uncertain value, and details the data in parameters to depend against attacks. With comparing our model with LDTS and Model using Trust Matrix, we conclude that our model has implemented a trade-offbetween detection rate and communication consumption.

关键词： Matrix algebra

来源：评论

学校读者我要写书评

暂无评论

A proof system in PADS

引用

10th International colloquium on Theoretical Aspects of computing, ICTAC 2013

作者： Yao, Xinghua Zhang, Min Chen, Yixiang MoE Engineering Research Center for Software/Hardware Co-design Technology and Application East China Normal University Shanghai China Shanghai Key Laboratory of Trustworthy Computing East China Normal University Shanghai China

ISBN: (纸本)9783642397172

The PADS (Process Algebra for Demand and Supply) framework is an approach to model resource demand and supply for the formal analysis of hierarchical scheduling. Inspired by the demand relation in PADS, we propose a weak demand relation covering several cases which can not be described by a demand relation. And we explore some properties of weak demand relation which are similar to properties of demand relation. Especially, if two tasks are in a weak demand relation then their schedulabilities are closely related. Furthermore, we present a proof system for the weak demand relation in a decomposing-composing way, which helps to compare two tasks' schedulabilities. Finally, we prove that the proof system is sound and complete with respect to the semantic definition of weak demand relation. © 2013 Springer-Verlag Berlin Heidelberg.

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：