The long-term ecosystem observation can provide data of water, soil, meteorology and biology to support ecosystem evaluation and management.At present, there is a lack of long-term observation data product system of ecosystem in China, so no effective guidance can be provided for the production of data products.Firstly the data product system of international eco-environmental research networks was analyzed.Then a long-term observation data product system of ecosystem based on the data product classification, data product gradation two dimensions was proposed, combining the existing long-term observation protocols and data resources of ecosystem in China.It could not only express the content of long-term observation data products, but also the process of data product production and processing, and had been applied to design the long-term observation data product system of forest ecosystem of Chinese ecosystem research network (CERN).This data product system has good practical value and will play an important role in improving the value of long-term observation data.

为提供更优质的使用Event-B形式化方法建模混合系统的工具,根据混合系统的时序约束建模方法,其能够很好刻画混合系统建模中的时间相关性质并且支持精化和组合,提出基于它的自动筛选、精化和组合的方法.开发对应的自动精化和组合的工具链,工具链包含模型检测、自动精化和组合、模型证明等一系列功能并拥有用户友好的界面.给出一个使用工具的案例介绍和应用此工具.

Hybrid and cyber-physical systems pose new challenges for formal construction of systems. In hybrid systems, the states evolve over continuous time according to related laws of continuous and discrete dynamics. Thus, timing constraints and synchronous signals play important roles. Moreover, in the development of complex hybrid systems, refinement, and composition of timing constraints are in need. However, the existing formal approaches of Event-B have difficulties in refinement and composition of hybrid systems. Therefore, in this article, we propose a formal hybrid approach to solve this problem. Our approach of modeling is based on the Event-B method, and uses the Rodin platform and its plugin Theory.

Event-B shared-variable and shared-event methods can decompose a large scale system into multiple subsystems and model them independently.Nevertheless,the existing Event-B method requires manual intervention to perform event composition among models.Therefore,this paper proposes a theory for the automated composition of models and develops an automated tool to improve the efficiency of model composition.With regard to the step-by-step introduction of module calls in the refinement model,this paper improves the PROG method and develops an automated refinement tool prototype.Through the two application case,the automated composition tool can compose events automately,the refinement tool reduces the call variables,which enhances the readability and maintainability of the system model.

Existing implementations of dynamic memory allocators (DMA) employ a large spectrum of policies and techniques. The formal specifications of these techniques are quite complicated in isolation and very complex when combined. Therefore, the formal reasoning on a specific DMA implementation is difficult for automatic tools and mostly single-use. This paper proposes a solution to this problem by providing formal models for a full class of DMA, the class using various kinds of lists to manage the memory blocks controlled by the DMA. To obtain reusable formal models and tractable formal reasoning, we organise these models in a hierarchy ranked by refinement relations. We prove the soundness of models and the refinement relations using the modeling framework Event-B and the theorem prover Rodin. We demonstrate that our hierarchy is a basis for an algorithm theory for list based DMA: it abstracts various existing implementations of DMA and leads to new DMA implementations. The applications of this formalisation include model-based code generation, testing, and static analysis.

Hybrid and cyberphysical systems pose significant challenges for formal development approaches based on pure discrete events. In this essay, after a brief look at the CPS landscape, the foundations of CPS systems are examined from the ground up, with a particular view to aspects rooted in the continuous part of the CPS spectrum. We take a journey starting from the foundations, through a number of ways of addressing the continuous mathematics aspects, to phenomena latent only in the world of physical descriptions, such as the onset of instability due to passing through bifurcation points in the problem parameter space. We argue that such phenomena, that can plague CPS design when optimising for performance metrics, can only be understood by sufficient engagement with the continuous world.

This case study of an insulin pump is to describe our solution of the following difficulties. Firstly, how to model features to obtain a family of products. Secondly, how to handle complex constraints and synchronization of components when composing features. Thirdly, how to construct the continuous environment for the individual features as well as for the composed system.

This paper presents the formal development of the memory management module of a real time operating system. The interesting feature of this type of memory manager is that its dynamic memory allocation/reallocation mechanism behaves in O(1) (no loops). This brings a serious challenge on the "correct by construction" approach used to build this kind of system. This is due to the necessity to elaborate some delicate algorithms associated with complex data structures. To overcome this challenge, we follow the refinement principles of Event-B: we construct the proved executable code from some initial requirements. This development is interesting because some of the encountered problems are rather necessary to be studied in formal proved developments, among which are a modular encapsulation development, the design pattern of a linked list, and the usage of guarded events to develop pre-conditioned operations. It also gives us the opportunity to study a complex program construction in some general terms going beyond this specific example.

While many systems are naturally viewed as the interaction between a controller subsystem and a controlled, or plant subsystem, they are often most easily initially understood and designed monolithically, simply as a collection of variables that represent various aspects of the system, which interact in the most self-evident way. A practical implementation needs to separate controller from plant though. We study the problem of when a monolithic ASM system can be split into controller and plant subsystems along syntactic lines derived from variables' natural affiliations. We give restrictions that enable the split to be carried out cleanly, and we give conditions that ensure that the resulting pair of controller and plant subsystems have the same behaviours as the original design. We relate this phenomenon to the concept of complete refinement in ASM. Making this strategy work effectively, usually requires a nontrivial domain theory, into which a number of properties which are neither the sole possession of the controller subsystem nor of the plant subsystem must be placed. We argue that these properties are latent in the original monolithic model. We illustrate the theory with a case study concerning eating with chopsticks. This leads to an extension of controller synthesis for continuous ASM systems, which are briefly covered. The chopsticks case study is then extended into the continuous sphere. (C) 2014 Elsevier B.V. All rights reserved.

This paper describes the modeling, done using the Event-B notation, of the aircraft landing gear case study that was proposed in a special track of the ABZ'2014 Conference. In the course of our development, we discovered some problems in our initial modeling approach. This has led us to propose a second approach and then a third one. Each approach is more efficient than the previous one in terms of proof obligations (roughly speaking: 2000, 1000, 500). All this will be described in this paper. The methodology of proving reachability and deadlock freeness are discussed. Animation and simulation are used as complementary analysis to formal proofs. We also try to go beyond this specific case study and give some thoughts about large industrial modeling.

The cardiac pacemaker system, proposed as a problem topic in the Verification Grand Challenge, offers a range of difficulties to address for formal specification, development, and verification technologies. We focus on the sensing problem, the question of whether the heart has produced a spontaneous heartbeat or not. This question is plagued by uncertainties arising from the often unpredictable environment that a real pacemaker finds itself in. We develop a time domain tracking approach to this problem, as a complement to the usual frequency domain approach most frequently used. We develop our case study in the continuous ASM (Abstract State Machine) formalism, which is briefly summarised, through a series of refinement and retrenchment steps, each adding new levels of complexity to the model.

A very simple model for train stopping is used as a vehicle for investigating how the development of a control system, initially designed in the continuous domain and subsequently discretized, can be captured within a formal development process compatible with standard model based refinement methodologies. Starting with a formalized requirements analysis using KAOS, an abstract model of the continuous system is created in the ASM formalism. This requires extensions of the KAOS and ASM formalisms, capable of dealing with quantities evolving continuously over real time, which are developed. After considering how the continuous system, described as a continuous control system in the state space framework, can be discretized, a discrete control system is created in the state space framework. This is re-expressed in the ASM formalism. The rigorous results on the relationship between continuous and discrete control system models that are needed to establish provable properties of the discretization, then become the ingredients of a retrenchment between continuous and discrete ASM models, and are thus fully integrated into the formal development. The discrete ASM model can then be further refined towards implementation.

This paper contains a further contribution to the handling of hybrid systems as presented in [3]. This time we insist on the usage of multiple methodologies involving not only refinements and proofs as in Event-B and the Rodin Platform, but also Matlab simulation, Animation, and Invariant discovery. We believe that a successful understanding of hybrid systems has to be done in this way by involving several distinct methodologies that are complementary. The paper also presents many examples illustrating the approach.

The ASM framework is extended to include continuously varying quantities as well as conventional discretely changing ones. This opens the door to the more faithful modeling of many scenarios where digital systems have to interact with the continuously varying physical world. Transitions in the extended framework are thus either moded (for discontinuous changing quantities), or pliant (for smoothly changing quantities). Refinement and retrenchment are defined in the extended context. The framework is used to develop a fragment of a simple system for the sensing problem for cardiac pacemakers, in the context of the pacemaker verification challenge.

This paper contains the development of hybrid systems in Event-B and the Rodin Platform. It follows the seminal approach introduced at the turn of the century in Action Systems. Many examples illustrate our approach.

Universities are actively exploring and implementing the cooperation courses with enterprises. In software engineering, the key construction is to build a win-win course to meet the needs of student development and enterprise requirements. This paper introduces a co-teaching curriculum model aimed at narrowing the theory-practice gap. The course construction system and diversified teaching methods are given based on actual experience of school-enterprise cooperation. The feed-back institution is necessary to check the effects of cooperation course. The establishment of integrated cooperation curriculum is helpful to develop innovative, practical and versatile international software engineers.

While many systems are naturally viewed as the interaction between a controller subsystem and a controlled, or plant subsystem, they are often most easily understood and designed monolithically. A practical implementation needs to separate controller from plant. We study the problem of when a monolithic ASM system can be split into controller and plant subsystems along syntactic lines derived from variables' natural affiliations. We give restrictions that enable the split to be carried out cleanly, and we give conditions that ensure that the resulting pair of controller and plant subsystems have the same behaviours as the original design. We illustrate the theory with a case study concerning eating with chopsticks. This leads to an extension of controller synthesis for continuous ASM systems, which are briefly covered. The case study is then extended into the continuous sphere.

It is a challenge to recommend Web services under multiple contexts. To address this challenge, we propose a context-aware collaborative filtering (CaCF) approach for service recommendation. Three types of contextual information, i.e. time, location and interest of user, are considered. In this approach, users' interests are extracted from service invocation records and represented as term-weight vectors. Neighbors are chosen according to the Cosine similarities of these vectors. Then, neighbors are filtered into close neighbors by location and time. At last, these close neighbors recommend service to a target user. We evaluate our method through comparing with other service recommendation approaches. The experimental results show that it achieves better precision and satisfaction rate than other two methods.

Including provision for continuously varying behaviour as well as discrete state change is considered for Event-B. An extension of Event-B is sketched that accommodates continuous events (called pliant events) in between familiar discrete events (called mode events).

Formally capturing the transition from a continuous model to a discrete model is investigated using model based refinement techniques. A very simple model for stopping (eg. of a train) is developed in both the continuous and discrete domains. The difference between the two is quantified using generic results from ODE theory, and these estimates can be compared with the exact solutions. Such results do not fit well into a conventional model based refinement framework; however they can be accommodated into a model based retrenchment. The retrenchment is described, and the way it can interface to refinement development on both the continuous and discrete sides is outlined. The approach is compared to what can be achieved using hybrid systems techniques.