Software for an air pollution measuring system: An application of modula

The program for a small embedded computer system has been implemented in Modula. The execution speed of this program was particularly important and the speed achieved was adequate. Some parts of this program are described using a notation derived from the Mascot approach. The use of the Mascot notation with a module-structured language is discussed and some suggestions for an appropriate style are made. Some simple optimizations of the program were made in order to achieve increased execution speed and it was observed that the final program ran at about twenty times the rate of an equivalent Fortran program. Some points on the suitability of Modula are briefly discussed and, in a similar way to previous authors, it is concluded that Modula is suitable for applications of this type.     

Safety verification and reachability analysis for hybrid systems

Safety verification and reachability analysis for hybrid systems is a very active research domain. Many approaches that seem quite different, have been proposed to solve this complex problem. This paper presents an overview of various approaches for autonomous, continuous-time hybrid systems and presents them with respect to basic problems related to verification.     

LMNtal as a hierarchical logic programming language

LMNtal (pronounced “elemental”) is a simple language model based on hierarchical graph rewriting that uses logical variables to represent connectivity and membranes to represent hierarchy. LMNtal is an outcome of the attempt to unify constraint-based concurrency and Constraint Handling Rules (CHR), the two notable extensions to concurrent logic programming. LMNtal is intended to be a substrate language of various computational models, especially those addressing concurrency, mobility and multiset rewriting. Although the principal objective of LMNtal was to provide a unifying computational model, it is of interest to equip the formalism with a precise logical interpretation. In this paper, we show that it is possible to give LMNtal a simple logical interpretation based on intuitionistic linear logic and a flattening technique. This enables us to call LMNtal a hierarchical, concurrent linear logic language.     

A hierarchical optimization neural network for large-scale dynamic systems

A recurrent neural network for dynamical hierarchical optimization of nonlinear discrete large-scale systems is presented. The proposed neural network consists of hierarchically structured sub-networks: one coordination sub-network at the upper level and several local optimization sub-networks at the lower level. In particular, the coordination sub-network and the local optimization sub-networks work simultaneously. This feature makes the proposed method outperform in computational efficiency the conventional iterative algorithms where there usually exists an alternately waiting time during the coordination and local optimization processes. Moreover, the state equations of the subsystems of the large-scale system are imbedded into their corresponding local optimization sub-networks. This imbedding technique not only overcomes the difficulty in treating the constraints imposed by the state equations, but also leads to significant reduction in the network size. We present stability analysis to prove that the neural network is asymptotically stable and this stable state corresponds to the optimal solution to the original optimal control problem. Finally, we illustrate the performance of the proposed method by an example.     

Non-homogeneous hierarchical Continuous Time Markov Chains

This paper shows a method of calculating the hazard rate of the non-homogeneous Markov chains using different homogeneous probability matrices for several hundreds small time intervals (using default parameters settings — the number of the intervals can be adjusted to balance accuracy/time-consumption ratio). The method is compared to a pessimistic method based on homogeneous Markov chains and used to calculate the hazard rate of the hierarchical Markov chain. The hazard rates of the blocks are calculated independently and the non-homogeneous approach allows us to use them to calculate the hazard rate of the whole system. The independent calculations are significantly faster than the calculation of a single model composed of all models of the blocks.     

面向分级身份密码批验签的错误签名混合筛选算法

针对分级身份密码（HIBC）批验签过程中的错误签名快速识别问题,设计实现了一种错误签名混合筛选算法。针对HIBC签名算法不完全聚合的特点,首先将所有签名作为树叶构造平衡二叉树,然后通过拆分攻克与指数测试方法查找错误签名,并且利用计算中间值的关联性减少计算开销。算法性能分析表明,当批验签中错误签名数大于2时,该算法计算开销低于独立测试、通用折半拆分、指数测试以及裁剪搜索算法,能够有效筛选出HIBC批验签中的错误签名,可以应用在云计算认证等应用场景中。     

基于递阶分解聚类的非线性系统递推模糊辨识

提出一种基于递阶分解聚类的递推模糊辨识方法．采用半模糊化方法对论域内的样本进行归类,根据各子集“线性化”程度评判模糊聚类的有效性,通过对性能最差的子集进行分解并辨识新增子模型的参数,逐步完成整个样本空间的模糊划分和模型辨识过程．在线辨识时采用递推最小二乘算法对模糊规则进行修正,同时可根据建模精度的要求删除性能最差的规则,并确立新模糊规则．仿真研究表明了该方法的有效性．     

Multi-level hierarchical interface-based supervisory control

Hierarchical Interface-Based Supervisory Control employs interfaces that allow properties of a monolithic system to be verified through local analysis. By avoiding the need to verify properties globally, significant computational savings can be achieved. In this paper we provide local requirements for a multi-level architecture employing command-pair type interfaces. This multi-level architecture allows for a greater reduction in complexity and improved reconfigurability over the two-level case that has been previously studied since it allows the global system to be partitioned into smaller modules. This paper also provides results for synthesizing supervisors in the multi-level architecture that are locally maximally permissive with respect to a given specification and set of interfaces.     

PHAVer: algorithmic verification of hybrid systems past HyTech

In 1995, HyTech broke new ground as a potentially powerful tool for verifying hybrid systems. But due to practical and systematic limitations it is only applicable to relatively simple systems. We address the main problems of HyTech with PHAVer, a new tool for the exact verification of safety properties of hybrid systems with piecewise constant bounds on the derivatives, so-called linear hybrid automata. Affine dynamics are handled by on-the-fly overapproximation and partitioning of the state space based on user-provided constraints and the dynamics of the system. PHAVer features exact arithmetic in a robust implementation that, based on the Parma Polyhedra Library, supports arbitrarily large numbers. To force termination and manage the complexity of the polyhedral computations, we propose methods to conservatively limit the number of bits and constraints of polyhedra. Experimental results for a navigation benchmark and a tunnel diode circuit demonstrate the effectiveness of the approach. A preliminary version of this paper appeared in the Proceedings of Hybrid Systems: Computation and Control (HSCC 2005), Lecture Notes in Computer Science 3414, Springer-Verlag, 2005, pp. 258–273.     

A verification framework for spatio-temporal consistency language with CCSL as a specification language

The Spatio-Temporal Consistency Language(STeC)is a high-level modeling language that deals natively with spatio-temporal behaviour,i.e.,behaviour relating to certain locations and time.Such restriction by both locations and time is of first importance for some types of real-time systems.CCSL is a formal specification language based on logical clocks.It is used to describe some crucial safety properties for real-time systems,due to its powerful expressiveness of logical and chronometric time constraints.We consider a novel verification framework combining STeC and CCSL,with the advantages of addressing spatio-temporal consistency of system behaviour and easily expressing some crucial time constraints.We propose a theory combining these two languages and a method verifying CCSL properties in STeC models.We adopt UPPAAL as the model checking tool and give a simple example to illustrate how to carry out verification in our framework.     

An efficient and non-interactive hierarchical key agreement protocol

The non-interactive identity-based key agreement schemes are believed to be applicable to mobile ad-hoc networks (MANETs) that have a hierarchical structure such as hierarchical military MANETs. It was observed by Gennaro et al. (2008) that there is still an open problem on the security of the existing schemes, i.e., how to achieve the desirable security against corrupted nodes in the higher levels of a hierarchy? In this paper, we propose a novel and very efficient non-interactive hierarchical identity-based key agreement scheme that solves the open problem and outperforms all existing schemes in terms of computational efficiency and data storage.     

A simpler minimum spanning tree verification algorithm

The problem considered here is that of determining whether a given spanning tree is a minimal spanning tree. In 1984 Komlós presented an algorithm which required only a linear number of comparisons, but nonlinear overhead to determine which comparisons to make. We simplify his algorithm and give a linear-time procedure for its implementation in the unit cost RAM model. The procedure uses table lookup of a few simple functions, which we precompute in time linear in the size of the tree.     

Synthesis of hierarchical systems

In automated synthesis, given a specification, we automatically create a system that is guaranteed to satisfy the specification. In the classical temporal synthesis algorithms, one usually creates a “flat” system “from scratch”. However, real-life software and hardware systems are usually created using preexisting libraries of reusable components, and are not “flat” since repeated sub-systems are described only once.In this work we describe an algorithm for the synthesis of a hierarchical system from a library of hierarchical components, which follows the “bottom-up” approach to system design. Our algorithm works by synthesizing in many rounds, when at each round the system designer provides the specification of the currently desired module, which is then automatically synthesized using the initial library and the previously constructed modules. To ensure that the synthesized module actually takes advantage of the available high-level modules, we guide the algorithm by enforcing certain modularity criteria.We show that the synthesis of a hierarchical system from a library of hierarchical components is Exptime-complete for μ-calculus, and 2Exptime-complete for Ltl, both in the cases of complete and incomplete information. Thus, in all cases, it is not harder than the classical synthesis problem (of synthesizing flat systems “from scratch”), even though the synthesized hierarchical system may be exponentially smaller than a flat one.     

A behavioral analysis and verification approach to pattern-based design composition

Integrating software components to produce large-scale software systems is an effective way to reuse experience and reduce cost. However, unexpected interactions among components when integrated into software systems are often the cause of failures. Discovering these composition errors early in the development process could lower the cost and effort in fixing them. This paper introduces a rigorous analysis approach to software design composition based on automated verification techniques. We show how to represent, instantiate and integrate design components, and how to find design composition errors using model checking techniques. We illustrate our approach with a Web-based hypermedia case study.     

A new hierarchical triangle-based point-in-polygon data structure

The point-in-polygon or containment test is fundamental in computational geometry and is applied intensively in geographical information systems. When this test is repeated several times with the same polygon a data structure is necessary in order to reduce the linear time needed to obtain an inclusion result. In the literature different approaches, like grids or quadtrees, have been proposed for reducing the complexity of these algorithms. We propose a new data structure based on hierarchical subdivisions by means of tri-cones, which reduces the time necessary for this inclusion test. This data structure, named tri-tree, decomposes the whole space by means of tri-cones and classifies the edges of the polygon. For the inclusion test only the edges classified in one tri-cone are considered. The tri-tree has a set of properties which makes it specially suited to this aim, with a similar complexity to other data structures, but well suited to polygons which represent regions. We include a theoretical and practical study in which the new data structure is compared with classical ones, showing a significant improvement.     

A hierarchical model of a linguistic variable

In this work a theoretical hierarchical model of dichotomous linguistic variables is presented. The model incorporates certain features of the approximate reasoning approach and others of the Fuzzy Control approach to Fuzzy Linguistic Variables. It allows sharing of the same hierarchical structure between the syntactic definition of a linguistic variable and its semantic definition given by fuzzy sets. This fact makes it easier to build symbolic operations between linguistic terms with a better grounded semantic interpretation. Moreover, the family of fuzzy sets which gives the semantics of each linguistic term constitutes a multiresolution system, and thanks to that any fuzzy set can be represented in terms of the set of linguistic terms. The model can also be considered a general framework for building more interpretable fuzzy linguistic variables with a high capacity of accuracy, which could be used to build more interpretable Fuzzy Rule Based Systems (FRBS).     

Abstraction-based verification of codiagnosability for discrete event systems

In this paper, we investigate the verification of codiagnosability for discrete event systems (DES). That is, it is desired to ascertain if the occurrence of system faults can be detected based on the information of multiple local sites that partially observe the overall DES. As an improvement of existing codiagnosability tests that resort to the original DES with a potentially computationally infeasible state space, we propose a method that employs an abstracted system model on a smaller state space for the codiagnosability verification. Furthermore, we show that this abstraction can be computed without explicitly evaluating the state space of the original model in the practical case where the DES is composed of multiple subsystems.     

基于FPGA的SoC/IP 验证平台的设计与应用

采用Altera公司CycloneII系列的FPGA设计了一个基于片上总线的SoC原型验证平台,并将VxWorks嵌入式操作系统应用于此平台,通过软硬件协同验证方法,验证了平台的可靠性。该平台在CF卡及通用智能卡SoC芯片验证中得以应用。