基于平滑调度的弱硬实时系统约束规范

约束规范是弱硬实时系统研究的基础。从弱硬实时系统的定义出发,提出了一个新的约束规范,它能够有效实现平滑调度。给出并证明了弱硬实时系统约束规范严格性比较的一个重要定理。业已证明,该约束规范具有良好的性能和较好的适用范围。     

γ演算到Action演算的转换

Action演算簇(action calculi)作为描述不同并发交互行为的数学框架,可以表示一大类具有某些相同特性的并发形式化模型.试图把(演算(一种基于约束的高阶并发计算模)也包含在action演算簇的框架下.首先定义了一个具体的action演算AC(K_γ),然后给出了从(演算到AC(K_γ)转换的形式描述,最后在定义AC(K_γ)的可观察性、弱互模拟关系和弱等价关系的基础上,以(演算为中间表示,证明了这种转换保持了(演算的弱行为等价性.研究表明,action演算簇可以表示基于约束的并发模型,从而充分说明了action演算簇的描述能力,并且为在action演算簇框架下把(演算与其他并发模型结合并进行比较提供了前提.     

基于path RTL的弱硬实时系统

弱硬实时系统是实时系统中的一个重要研究领域.经典弱硬实时系统以任务流中任务满足或错过的个数来约束系统性能,存在着无法准确表达系统实时特性的不足,以及弱硬实时的可靠性无法证明的缺陷.通过提出弹性截止期的概念,定义基于path RTL的弱硬实时系统,有效解决了经典弱硬实时系统可靠性无法证明的难题;实现了弱硬实时系统的约束由时间特性来表达的目标;对于新兴出现的弱硬实时应用提供了完整的解决方案;同时也对经典弱硬实时系统提出了规约算法,以充分利用经典弱硬实时系统在约束规范、调度算法等方面已有研究成果.通过比较,path RTL弱硬实时系统在系统完整性、系统可靠性和应用领域等方面,比经典弱硬实时系统具有优势.     

一种弱硬实时约束规范

当弱硬实时系统约束规范中μ-patterns首个字符为0时,弱硬实时约束规范 就失去作用。针对该问题,通过改变截止期满足率的计算方法,提出一个弱硬实时约束规范 ,在保持 优点的同时,扩大了其使用范围,并通过偏序证明来保证其优良 性能。     

（m，p1）约束规范的动态调度算法研究

（m,p¹）有效解决了µ-pattern中第一个数字为0时部分约束规范失效的问题。在弱硬实时调度算法研究的基础上,针对（m,p¹）约束规范,提出了一个动态弱硬实时调度算法,分析与仿真结果表明,算法效果良好。     

一种弱硬实时约束规范(-m,P1)

当弱硬实时系统约束规范中μ-patterns首个字符为0时,弱硬实时约束规范(-m,P)就失去作用.针对该问题,通过改变截止期满足率的计算方法,提出一个弱硬实时约束规范(-m,P1),在保持(-m,p)优点的同时,扩大了其使用范围,并通过偏序证明来保证其优良性能.     

相接行凸约束网络的快速识别算法

约束网络为计算机科学中的许多问题提供了一种有效的表示方法.一般而言,约束满足问题是NP完全的.然而,许多实际问题通常对约束的结构或形式施加了特殊的限制,从而能够高效地加以解决.迄今,为了识别易处理约束类,人们对特殊的约束或约束网络方面进行了许多研究.相接行凸(connected row-convex,简称CRC)约束网络是Deville等人提出的一类易处理问题.为了给该类问题寻求有效的快速识别算法,在CRC约束网络相关工作基础上,提出了CRC约束矩阵的标准型.在分析CRC约束矩阵的标准型性质的基础上,利用行凸(row-convex,简称RC)约束网络的判定,结合PQ树(由P节点和Q节点构成的树)的性质和矩阵的索引表示法,给出了CRC约束网络的快速识别算法.该算法的时间复杂度为O(n³d²),其中,n为约束网络涉及的变量数,d为各变量的定义域中最大定义域的大小.该时间复杂度达到该类问题的最佳时间复杂度,从而为实际的CRC约束满足问题的求解提供了可行的方法.     

(m-,P1)约束规范的动态调度算法研究

(m,p1)有效解决了μ-pattern中第一个数字为0时部分约束规范失效的问题。在弱硬实时调度算法研究的基础上,针对(m,p1)约束规范,提出了一个动态弱硬实时调度算法,分析与仿真结果表明,算法效果良好。     

带尺寸约束的弱监督眼底图像视盘分割

目的 医学图像的像素级标注工作需要耗费大量的人力。针对这一问题，本文以医学图像中典型的眼底图像视盘分割为例，提出了一种带尺寸约束的弱监督眼底图像视盘分割算法。方法 对传统卷积神经网络框架进行改进，根据视盘的结构特点设计新的卷积融合层，能够更好地提升分割性能。为了进一步提高视盘分割精度，本文对卷积神经网络的输出进行了尺寸约束，同时用一种新的损失函数对尺寸约束进行优化，所提的损失公式可以用标准随机梯度下降方法来优化。结果 在RIM-ONE视盘数据集上展开实验，并与经典的全监督视盘分割方法进行比较。实验结果表明，本文算法在只使用图像级标签的情况下，平均准确识别率（mAcc）、平均精度（mPre）和平均交并比（mIoU）分别能达到0.852、0.831、0.827。结论 本文算法不需要专家进行像素级标注就能够实现视盘的准确分割，只使用图像级标注就能够得到像素级标注的分割精度。缓解了医学图像中像素级标注难度大的问题。     

支持多约束的K-匿名化方法

K-匿名化(K-anonymization)是数据发布环境下保护数据隐私的一种重要方法.目前,K-匿名化方法主要针对单一约束条件进行处理,而实际应用中涉及到大量的多约束条件,使K-匿名化问题更加复杂.如果简单地将单一约束K-匿名化方法应用到多约束情况,会造成大量的信息损失及过低的处理效率.根据多约束之间的关系,通过继承Classfly算法的元组概括过滤思想,提出多约束K-匿名化方法Classfly⁺及相应的3种算法,包括朴素算法、完全IndepCSet算法和部分IndepCSet的Classfly⁺算法.实验结果显示,Classfly⁺能够很好地降低多约束K-匿名化的信息损失,改善匿名化处理的效率.     

Generation of test sequences from formal specifications: GSM 11‐11 standard case study

This paper presents the results of a case study on generating test cases for a fragment of the smart card GSM 11‐11 standard. The generation method is based on an original approach using the B notation and techniques of constraint logic programming with sets. The GSM 11‐11 technical specifications were formalized with the B notation. From this B specification, a system of constraints was derived, equivalent to this formal model. Using a set constraint solver, boundary states were computed and test cases were obtained by traversing the constrained reachability graph of the specifications. The purpose of this project was to evaluate the contribution of this testing environment, called B ‐TESTING ‐TOOLS , in an industrial process on a real life‐size application, by comparing the generated test sequences with the already used and high‐quality manually‐designed tests. This comparison enabled us to validate our approach and showed its effectiveness in the validation process of critical applications: the case study gives a wide coverage (about 85%) of the generated tests compared to the pre‐existing tests and a saving of 30% in test design time. Copyright © 2004 John Wiley & Sons, Ltd.     

Knowledge-based construction of distributed constrained systems

The problem of deriving distributed implementations from global specifications has been extensively studied for a number of application domains. We explore it here from the knowledge perspective: A process may decide to take a local action when it has enough knowledge to do so. Such knowledge may be acquired by communication through primitives available on the platform or by static analysis. In this paper, we want to combine control and distribution, that is, we need to impose some global control constraint on a system executed in a distributed fashion. To reach that goal, we compare two approaches: either build a centralized controlled system, distribute its controller and then implement this controlled system on a distributed platform; or alternatively, directly enforce the control constraint while implementing the distributed system on the platform. We show how to achieve a solution following the second approach and explain why this is a pragmatic and more efficient strategy than the other, previously proposed one.     

An Improved Anti‐Windup Bumpless Transfer Structures Design for Controllers Switching

In this paper, an anti‐windup bumpless transfer (AWBT) control structure combined with linear interpolation method is proposed for smooth switching control. By choosing an appropriate scheduling signal, different controllers can be switched smoothly under a unified framework. Meanwhile, some robust specifications including H₂/H_∞ performance, pole placement constraint, and passivity of the closed‐loop system can be preserved through controller switching. Furthermore, for the linear system subject to input saturation, the stability and L₂ gain of the closed‐loop system can be guaranteed. Finally, a cart‐spring pendulum system is simulated to demonstrate the effectiveness of the proposed scheme.     

CLPS–B – A constraint solver to animate a B specification

This paper proposes an approach to evaluating B formal specifications using constraint logic programming with sets (CLPS). This approach is used to animate and generate test sequences from B formal specifications. The solver, called CLPS–B, is described in terms of constraint domains, consistency verification, and constraint propagation. It is more powerful than most constraint systems because it allows the domain of variable to contain other variables, which increases the level of abstraction. The constrained state propagates the nondeterminism of the B specifications and reduces the number of states in a reachability graph. We illustrate this approach by comparing the constrained state graph exploration with the concrete one in a simple example – process scheduler. We also describe the automated test generation method that uses the CLPS–B solver to better control combinational explosion.     

Compilation of Constraint Programs with Noncyclic and Cyclic Dependencies to Procedural Parallel Programs

This paper reports on a compiler for translation of constraint specifications into procedural parallel programs. A constraint program in our system consists of a set of constraints and an input set containing a subset of the variables appearing in the constraints. The compiler described in this paper successfully compiles a substantially larger class of constraint specifications to efficient programs than did its predecessors. In particular the compiler has been extended to generate processor and memory efficient programs for cyclic constraints which can be resolved by computational relaxation methods. The paper first details the basic compilation process for noncyclic constraints. It then describes the additional steps in the compilation process which enable resolution of cyclic constraints to iterative computational processes and illustrates the process using derivation of a parallel program for solution of the Laplace equation as the example.     

Efficient analysis of pattern-based constraint specifications

Precision and consistency are important prerequisites for class models to conform to their intended domain semantics. Precision can be achieved by augmenting models with design constraints and consistency can be achieved by avoiding contradictory constraints. However, there are different views of what constitutes a contradiction for design constraints. Moreover, state-of-the-art analysis approaches for proving constrained models consistent either scale poorly or require the use of interactive theorem proving. In this paper, we present a heuristic approach for efficiently analyzing constraint specifications built from constraint patterns. This analysis is based on precise notions of consistency for constrained class models and exploits the semantic properties of constraint patterns, thereby enabling syntax-based consistency checking in polynomial-time. We introduce a consistency checker implementing these ideas and we report on case studies in applying our approach to analyze industrial-scale models. These studies show that pattern-based constraint development supports the creation of concise specifications and provides immediate feedback on model consistency.     

Stabilizing and robust fractional order PI controller synthesis for first order plus time delay systems

For all the stable first order plus time delay (FOPTD) systems, a fractional order proportional integral (FOPI) or a traditional integer order proportional integral derivative (IOPID) controller can be designed to fulfill a flat phase constraint and two design specifications simultaneously: gain crossover frequency and phase margin. In this paper, a guideline for choosing two feasible or achievable specifications, and a new FOPI/IOPID controller synthesis are proposed for all the stable FOPTD systems. Using this synthesis scheme, the complete feasible region of two specifications can be obtained and visualized in the plane. With this region as the prior knowledge, all combinations of two specifications can be verified before the controller design. Especially, it is interesting to compare the areas of these two feasible regions for the IOPID and FOPI controllers. This area comparison reveals, for the first time, the potential advantages of one controller over the other in terms of achievable performances. A simulation illustration is presented to show the effectiveness and the performance of the designed FOPI controller compared with the optimized integer order PI controller and the IOPID controller designed following the same synthesis for the FOPI in this paper.     

A high-level Petri nets-based approach to verifying task structures

As knowledge-based system technology gains wider acceptance, there is an increasing need to verify knowledge-based systems to improve their reliability and quality. Traditionally, attention has been given to verifying knowledge-based systems at the knowledge level, which only addresses structural errors such as redundancy, conflict and circularity in rule bases. No semantic errors (such as inconsistency at the requirements specification level) have been checked. In this paper, we propose the use of task structures for modeling user requirements and domain knowledge at the requirements specification level, and the use of high-level Petri nets for expressing and verifying the task structure-based specifications. Issues in mapping task structures onto high-level Petri nets are identified, e.g. the representation of task decomposition, constraints and the state model; the distinction between the "follow" and "immediately follow" operators; and the "composition" operator in task structures. The verification of task structures using high-level Petri nets is performed on model specifications of a task through constraint satisfaction and relaxation techniques, and on process specifications of the task based on the reachability property and the notion of specificity     

Synthesis of fixed-structure robust controllers using a constrained particle swarm optimizer with cyclic neighborhood topology

The purpose of this paper is to develop design scheme based on an easy-to-use meta-heuristic approach with superior reliability and validity for fixed-structure robust controllers, satisfying both multiple control specifications and system stability conditions. For this purpose, a particle swarm optimizer is first developed, which reduces the probability of premature convergence to local optima in the PSO (particle swarm optimization) by exploiting the particle’s local social learning based on the idea of cyclic-network topology. Next, it is shown how to obtain a fixed-structure robust controller with constraints on multiple H_∞ specifications and system stability based on the developed PSO technique incorporated with a simple constraint handling method. Finally, typical numerical examples are studied to show the applicability of the proposed methodology to the synthesis of fixed-structure robust controllers. These examples clearly verify that the developed design scheme gives a novel and powerful impetus with remarkable reliability to fixed-structure robust controller syntheses.     

一种基于角色访问控制模型的约束规范描述

传统的访问控制主要有自主型的访问控制DAC(Discretionary Access Control)和强制型的访问控制MAC(Mandatory Access Control)。强制型访问控制是“强加”给访问主体的,即系统强制主体服从访问控制政策。自主型的访问控制是在确认主体身份以及它们所属的组的基础上,对访问进行限定的一种方法。随着企业规模的增大,企业的信息化管理变得越来越重要,企业级访问控制和安全管理设计将是最难解决的问题之一,DAC和MAC已不能满足需要。20世纪90年代