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

LTL model checking probabilistic Petri net system

International Journal of Advancements in Computing Technology 2012年第1期4卷 172-178页

作者： Liu, Yang Miao, Huaikou School of Computer Engineering and Science Shanghai University Shanghai 200072 China Shanghai Key Laboratory of Computer Software Evaluating and Testing Shanghai 200072 China School of Information Science and Technology Taishan University Taian Shandong 271021 China

Nonfunctional property verification is becoming more and more important to computer system. In recent decades, in order to describe not only the system function but also the system performance, researchers in the area of formal methods try to extend Petri net for modelling computer system, and the verification problem becomes the quantitative verification from the qualitative verification. In this paper, we define the reachability graph and present the solution algorithm to reachability graph;then we put forward an algorithm for linear-time temporal logic model checking probabilistic Petri net system;for demonstrating the effectiveness of this algorithm, we run an example in the modelling an verification tool which we developed.

关键词： Model checking

来源：评论

学校读者我要写书评

暂无评论

A formal aspect-oriented method to model and analyse secure service composition

引用

International Journal of Autonomous and Adaptive Communications Systems 2015年第2-3期8卷 119-140页

作者： Fan, Guisheng Yu, Huiqun Chen, Liqiong Liu, Dongmei Department of Computer Science and Engineering East China University of Science and Technology Shanghai200237 China Shanghai Key Laboratory of Computer Software Evaluating and Testing Shanghai201112 China Department of Computer Science and Information Engineering Shanghai Institute of Technology Shanghai200235 China

Service-oriented computing (SOC) is becoming a prominent paradigm for creating value-added enterprise applications by composing web services. However, this flexibility comes along with new security risks. In this paper, Petri nets are used to precisely describe the different components of service composition, such as service, component, the basic relation between components, etc. The dynamic matching strategy of service composition is proposed, aspect orientation is used to weave it into the base net, which includes evaluation concern, authorisation concern and failure processing concern, the weaving mechanism dynamically integrates these schemas into a secure aspect model. Based on this, the operation semantics and related theories of Petri nets help prove the effectiveness and feasibility of proposed method, the enforcement algorithm is also given. An example explains the modelling process of service composition, and a series of experiments are done to explain that the use of aspects for service composition is more efficient than conventional techniques. © 2015 Inderscience Enterprises Ltd.

关键词： Petri nets

来源：评论

学校读者我要写书评

暂无评论

An approach to analyzing time constrained service composition

引用

Journal of computers 2011年第8期6卷 1723-1731页

作者： Fan, Guisheng Yu, Huiqun Chen, Liqiong Tong, Ruan Department of Computer Science and Engineering East China University of Science and Technology Shanghai 200237 China Shanghai Key Laboratory of Computer Software Evaluating and Testing Shanghai 200237 China Department of Computer Science and Information Engineering Shanghai Institute of Technology Shanghai 200235 China

Service composition is widely applied in different applications. One key issue is how to model and analyze time-related properties for service composition. A model called service composition time-constrained Petri Net (SCTNet) is proposed in the paper, which is capable of capturing time behavior of services accurately. The basic relationships, priority and preemption between services are characterized, meanwhile the transaction properties of service are also considered. In order to reduce the state space of model, we propose four simplification schemas which can maintain structural feature and time delay of SCT-Net, a theorem is given to explain the rational of simplification schemas. We present the concept of the greatest concurrent set and analyze the consistency of overtime handling based on the state space of the model. Finally, a heuristic algorithm for schedule computation is created and the experiments are given to explain the feasibility of our method. © 2011 ACADEMY PUBLISHER.

关键词： Petri nets

来源：评论

学校读者我要写书评

暂无评论

An approach to analyzing user preference based dynamic service composition

Journal of Software

引用

Journal of software 2010年第9期5卷 982-989页

作者： Fan, Guisheng Yu, Huiqun Chen, Liqiong Yu, Caizhu Department of Computer Science and Engineering East China University of Science and Technology Shanghai 200237 China Shanghai Key Laboratory of Computer Software Evaluating and Testing Shanghai 201112 China Department of Computer Science and Information Engineering Shanghai Institute of Technology Shanghai 200235 China

As a way to compose independent service together to fulfill a function, service composition is an important means for flexible and rapid information integration of complex distribution application in open and heterogeneous environment. However, the diversity of requirements makes it difficult to guarantee the correctness of service composition. This paper proposes a hierarchical dynamic service composition net (HDSC-net), and user's preference based mechanism for service composition. HDSC-net is used to model operation, the relationships between operations, operation mapping, and user's preference. Transfer matrix is constructed to express the relationships between states, while theories of Petri nets help prove the composability of service. The strategy for dynamic service composition and its corresponding enforcement method are also proposed. A case study of Travel Service demonstrates the applicability of proposed method and its effectiveness. © 2010 Academy Publisher.

关键词： Web services

来源：评论

学校读者我要写书评

暂无评论

A MVC-based collaborative framework support for test suite

A MVC-based collaborative framework support for test suite

引用

International Conference on computer Supported Cooperative Work in Design

作者： Liu, Zhenyu Li, Ting Yang, Genxing School of Computer Science Fudan University Shanghai China Shanghai Software Industry Association Shanghai China Shanghai Key Laboratory of Computer Software Evaluating and Testing Shanghai China

ISBN: (纸本)9781424467631

Test design is the key of software testing. In order to improve utilization of test suite effectively, a reasonable and flexible architecture should be introduced to collaborate, manage and utilize the abundant test suite library in software test practice. This paper puts forward a novel software test suite, which uses a formal language definition. In the paper, a test suite design framework, which is based on model-view-controller pattern, is introduced. The framework can be used to separate test suite design, analysis and presentation. Also, the framework uses user-interface and filter method based on test suite library. The test suite library platform is a reliable and extensible web-based test suite collaborative application. © 2010 IEEE.

关键词： software testing

来源：评论

学校读者我要写书评

暂无评论

Comparison of query languages for semantic database models 2018

Comparison of query languages for semantic database models

引用

2018 International Conference on Computing and Data Engineering, ICCDE 2018

作者： Thiam, Ablaye Xu, Dong Miao, Huaikou Niu, Zhihua School of Computer Engineering and Science Shanghai University Shanghai200444 China Shanghai Key Laboratory of Computer Software Evaluating and Testing China

ISBN: (纸本)9781450363938

A basic model of data illustrates the logical structure of a database including the relations and the constraints which determine how the data is stored and its accessibility. Individual database models are based upon the rules and concepts of a broader data model adopted by designer. Most data models can be represented with basic tables and diagrams. This paper will address the data model semantic and their interaction with Query languages. It will also discuss the general methods for implementing data models and data concepts, as they are applied to a wide range of semantic data models. © 2018 Association for Computing Machinery.

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

Considering web frameset and browser interactions in modeling and testing of web applications

Considering web frameset and browser interactions in modelin...

引用

2009 International Conference on Computational Intelligence and software Engineering, CiSE 2009

作者： Song, Bo Miao, Huaikou Chen, Shengbo School of Computer Engineering and Science Shanghai University Shanghai 200072 China Shanghai Key Laboratory of Computer Software Evaluating and Testing China

ISBN: (纸本)9781424445073

Web frameset is used to organize multiple frames and nested framesets to make the layout of some Web pages more identical and bring the development of Web applications easier, which was wildly used in today's Web applications. Web applications can only be accessed through dedicated client systems called Web browsers. The behaviors of Web frameset and Web browser interactions influence the functionalities and navigation of Web applications. In this paper, special care on Web frameset and Web browser interactions is paid and an approach to modeling the Web application's navigation and test generation with Web frameset and browser interactions is proposed. The extended FSM is employed to formalize the navigation models and a FSM-TT (FSM Test-Tree) is constructed. At last, test generation is given out from FSM-TT which satisfies the corresponding coverage criteria. ©2009 IEEE.

关键词： Web browsers

来源：评论

学校读者我要写书评

暂无评论

Removing shift-variant motion blur from an image using Poisson interpolation

Removing shift-variant motion blur from an image using Poiss...

引用

MIPPR 2009 - Automatic Target Recognition and Image Analysis: 6th International Symposium on Multispectral Image Processing and Pattern Recognition

作者： Ren, Chunjian Huang, Yaping Liu, Xiaoqiang Qiao, Yi School of Computer Science and Technology Donghua University Shanghai China Shanghai Key Laboratory of Computer Software Evaluating and Testing Shanghai China

ISBN: (纸本)9780819478061

Photographs captured with sufficient exposure under low-light conditions are usually blurred if there are moving objects. Under some circumstances, the restoration is challenging because of complicated motion blur such as rotation and distortion. In this paper, we propose a novel method to replace the motion blur objects of blurred image with the corresponding sharp objects of flash image using Poisson interpolation. First, assisted by the sufficient exposure blurred image, we adopt graph-cut to minimize a simple cost function and extract the intensely lightened sharp objects in the flash image. Second, we interpolate the extracted sharp objects into the blurred image, and then remove the remnant blur around the sharp objects through gradient domain Poisson interpolation. Further, a simple method is designed that the user can interactively adjust the brightness and contrast of flash area in the synthetical image. The experiments demonstrate that our algorithms are efficient. © 2009 Copyright SPIE - The International Society for Optical Engineering.

关键词： Interpolation

来源：评论

学校读者我要写书评

暂无评论

testing web applications with web frameset and browser interactions

引用

Information Technology Journal 2011年第7期10卷 1305-1314页

作者： Song, Bo Chen, Shengbo College of Information Science and Technology Qingdao University of Science and Technology 266061 Qingdao China Shanghai Key Laboratory of Computer Software Evaluating and Testing 201112 Shanghai China School of Computer Engineering and Science Shanghai University 200072 Shanghai China

software testing is a difficult task and testing Web applications may be more difficult, due to their characteristics. Web application is an interactive one since it came into being. How to model and test Web interactions is a challenge in software engineering. Web navigation models are useful to clarify requirements and specify implementation behaviors. Web frameset and Web browser's interactions are wildly used in today's Web applications. The behaviors of Web frameset and Web browser interactions changed the traditional Web navigation and influence the functionalities of Web applications. In this study, we took Web frameset and Web browser's interactions into account and proposed an approach to modeling the Web application's navigation and generating tests with Web framesets and browser's interactions. The construction formal semantics of structure compositionof Web frameset is give out. Based on the formal semantics, the Web navigation with Web framesets is modeled. The Extended Browser Loading Model with Web frameset (EBLM) and the extended FSMis employed to formalize the navigation models with Web framesets and browser's interactions andaFSM Test-Tree (FSM-TT) is constructed using present construction algorithm. At last, test generation is given out which satisfies the corresponding coverage criteria. This study resolves the following research problems: (1) propose an approach tomodeling Web applications with Web framesets and Web browser's interactions, (2) give the formal construction semantics of Web frameset and (3) formalize the navigation model and generatingtests. © 2011 Asian Network for Scientific Information.

关键词： testing

来源：评论

学校读者我要写书评

暂无评论

Combining Product Line Approach and Formal Specification for Product Family Modeling 5

Combining Product Line Approach and Formal Specification for...

引用

5th IEEE International Conference on computer and Communications, ICCC 2019

作者： Wang, Xi Shanghai University School of Computer Engineering and Science Shanghai China Shanghai Key Laboratory of Computer Software Testing and Evaluating Shanghai201114 China

ISBN: (纸本)9781728147437

The lack of systematic approach for product family modeling leads to difficulties in developing a series of high-quality software products simultaneously. This paper tackles this challenge by combining product line approach and formal specification technique. After constructing the feature model of the target family, our approach will start the formalization of the bottom-level features. For each feature, a formal model will be built according to its inner structure and function details. Any problem occurred during this process will cause the evolvement of the feature model under the guidance of a set of pre-defined evolution rules. The final product family model will be established when no problem can be found in both feature model and feature specification. This interleaving of feature model evolvement and feature formalization facilitates consistent and complete product family modeling from both abstract and concrete levels. A case study is given to illustrate the validity of the approach. © 2019 IEEE.

关键词： Formal specification

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：