检索结果-南通市图书馆

Convergence and optimality of BS-type discrete hedging strategy under stochastic interest rate

在线全文

学校读者我要写书评

暂无评论

Science China Mathematics 2011年第7期54卷 1457-1478页

作者： he jifeng WU Lan Department of Mathematics Peking University Beijing 100871 China

We focus on the asymptotic convergence behavior of the hedging errors of European stock option due to discrete hedging under stochastic interest rates. There are two kinds of BS-type discrete hedging differ in hedging instruments: one is the portfolio of underlying stock, zero coupon bond, and the money market account (Strategy BSI); the other is the underlying stock, zero coupon bond (Strategy BSII). Similar to the results of the deterministic interest rate case, we show that convergence speed of the discounted hedging errors is 1/2-order of trading frequency for both strategies. Then, we prove each of the BS-type strategy is not only locally optimal, but also globally optimal under the corresponding measure. Finally, we give some numerical examples to illustrate the results. All the discussion is based on non-arbitrage condition and zero transaction cost.

关键词： discrete time hedging delta hedging stochastic interest rate

A UTP semantic model for Orc language with execution status and fault handling

在线全文

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2014年第5期8卷 709-725页

作者： Qin LI Yongxin ZHAO Huibiao ZHU jifeng he Software Engineering Institute East China Normal University Shanghai 200062 China

The Orc language is a concurrency calculus pro- posed to study the orchestration patterns in service oriented computing. Its special features, such as high concurrency and asynchronism make it a brilliant subject for studying web applications that rely on web services. The conventional se- mantics for Orc does not contain the execution status of ser- vices so that a program cannot determine whether a service has terminated normally or halted with a failure after it pub- lished some results. It means that this kind of failure cannot be captured by the fault handler. Furthermore, such a seman- tic model cannot establish an order saying that a program is better if it fails less often. This paper employs UTP methods to propose a denotational semantic model for Orc that con- rains execution status information. A failure handling seman- tics is defined to recover a failure execution back to normal. A refinement order is defined to compare two systems based on their execution failures. Based on this order, a system that introduces a failure recovery mechanism is considered bet- ter than one without. An extended operational semantics is also proposed and proven to be equivalent to the denotational semantics.

关键词： Orc language service oriented computing uni-fying theories of programming denotational semantics op-erational semantics

A strategy for service realization in service-oriented design

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Science in China(Series F) 2006年第6期49卷 864-884页

作者： LIU Jing he jifeng LIU Zhiming Software Engineering Institute East China Normal University Shanghai 200062 China International Institute of Software Technology United Nations University Macao China

Recently service orientation is becoming a mainstream approach for building large scale software systems. A key requirement in service-oriented design is the dependability of service. It stipulates that the behavior of services is controllable. Formal models can aid in constructing software in a dependable manner. They can describe ser- vices precisely and compose them together consistently. This paper presents a strategy for service realization based on a novel layered formal model. When a service is provided or required via internet, the semantic consistency becomes critical issue, Our architecture tackles the issue by proposing a novel scheme： defining contract of a service to keep semantic information. Although service-oriented design is our prime target, the contract models, to a large extent, are independent of the framework of design and therefore applicable to large scale software design in general.

关键词： service-oriented design interface contract component.

Hybrid MARTE statecharts

在线全文

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2013年第1期7卷 95-108页

作者： Jing LIU Ziwei LIU jifeng he Freederic MALLET Zuohua DING Shanghai Key Laboratory of Trustworthy Computing East China Normal University Shanghai 200062 China INRIA Sophia Antipolis M6diterran6e Sophia Antipolis 06902 France Center of Math Computing and Software Engineering Zhejiang Sci-Tech University Hangzhou 310018 China

The specification of modeling and analysis of real-time and embedded systems （MARTE） is an extension of the unified modeling language （UML） in the domain of real-time and embedded systems. Even though MARTE time model offers a support to describe both discrete and dense clocks, the biggest effort has been put so far on the specifi- cation and analysis of discrete MARTE models. To address hybrid real-time and embedded systems, we propose to ex- tend statecharts using both MARTE and the theory of hybrid automata. We call this extension hybrid MARTE statecharts. It provides an improvement over the hybrid automata in that： the logical time variables and the chronometric time vari- ables are unified. The formal syntax and semantics of hybrid MARTE statecharts are given based on labeled transition sys- tems and live transition systems. As a case study, we model the behavior of a train control system with hybrid MARTE statecharts to demonstrate the benefit.

关键词： UML MARTE hybrid automata hybrid MARTE statechart train control system

Automated coverage-driven testing: combining symbolic execution and model checking

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Science China(Information Sciences) 2016年第9期59卷 242-243页

作者： Ting SU Geguang PU Weikai MIAO jifeng he Zhendong SU Shanghai Key Laboratory of Trustworthy Computing East China Normal University Department of Computer Science University of California

Software testing is the primary way to ensure software quality,but occupies more than 50%the cost of software development[1].It was estimated that software failures cost the US economy alone about 60 billion each year... 详细信息

关键词： test combining symbolic execution and model checking Automated coverage-driven testing DSE code

AADL+: a simulation-based methodology for cyber-physical systems

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2019年第3期13卷 516-538页

作者： Jing LIU Tengfei LI Zuohua DING Yuqing QIAN Haiying SUN jifeng he Shanghai Key Laboratory of Trustworthy Computing East China Normal University Shanghai 200062 China Zhejiang Sci-Tech University Xiasha College Park Hangzhou 310018 China

AADL (architecture analysis and design language) concentrates on the modeling and analysis of application system *** is quite popular for its simple syntax,powerful functionality and extensibility and has been widely applied in embedded systems for its ***,it is not enough for AADL to model cyber-physical systems (CPS) mainly because it cannot be used to model the continuous dynamic *** paper proposes an approach to construct a new sublanguage of AADL called AADL+,to facilitate the modeling of not only the discrete and continuous behavior of CPS,but also interaction between cyber components and physical *** syntax and semantics of the sublanguage are provided to describe the behaviors of the ***'s more,we develop a plug-in to OSATE (open-source AADL tool environment) for the modeling of *** the plug-in supports syntax checking and simulation of the system model through linking with ***,the AADL+ annex is successfully applied to model a lunar rover control system.

关键词： AADL cyber-physical systems (CPS) simulation OSATE lunar rover control system

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

A novel requirement analysis approach for periodic control systems

在线全文

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2013年第2期7卷 214-235页

作者： Zheng WANG Geguang PU Jiangwen LI Yuxiang CheN Yongxin ZHAO Mingsong CheN Bin GU Mengfei YANG jifeng he Shanghai Key Laboratory of Trustworthy Computing Software Engineering Institute East China Normal UniversityChina Shanghai 200241 Beijing Institute of Control Engineering China Beijing 100080 School of Computing National University of SingaporeSingapore Singapore 119077 China Academy of Space Technology China Beijing 100094

Periodic control systems （PCSs） are widely used in real-time embedded system domain. However, traditional manual requirement analysis assumes the expert knowledge, which is laborious and error-prone. This paper proposes a novel requirement analysis approach, which supports the automated validation of the informal requirement specifi- cations. Based on the normalized initial requirement docu- ments, our approach can construct an intermediate SPARDL model with both formal syntax and semantics. To check the overall system behaviors, our approach can transform the SPARDL models into executable code for simulation. The derived prototype simulator from SPARDL models enables the testing-based system behavior validation. Moreover, our approach enables the analysis of the dataflow relations in SPARDL models. By revealing input/output and affecting re- lations, our dataflow analysis techniques can help software engineers to figure out the potential data dependencies be- tween SPARDL modules. This is very useful for the module reuse when a new version of the system is developed. A study of our approach using an industry design demonstrates the practicality and effectiveness of our approach.

关键词： SPARDL simulation dataflow analysis codegeneration

East Asia Mayors' Forum held in Kunming

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Voice of Friendship 2004年第2期 11-13页

作者： he jifeng

After more than one year’s preparation, the first East Asia Mayors’ Forum (EAMF)was held in Kunming of Yunnan Province on December 2, 2003. Mayors or representatives from 23 cities of 11 countries, namely Bandar Seri Begawan, Kuala Belait and Seria and Tutong of Brunei, Phnom Penh, Battambang and Siemreap Province of Cambodia, Surabaya of Indonesia,

关键词： Kunming visited Myanmar ASEAN administration dialo