Cost enforcement in the real-time specification for Java

The Real-Time Specification for Java (RTSJ) provides an integrated approach to scheduling periodic real-time threads and monitoring their CPU execution time. It defines a cost enforcement model whereby a periodic real-time thread is suspended when it consumes more CPU time (budget) than it requested in a single release. However, compliant implementations need not support this model, as the underlying operating systems mechanisms are not widely available. Consequently, experience with the model is limited (it is generally not provided in most implementations of the RTSJ). In previous work we showed, using model checking techniques, that the current version of the cost enforcement model can, under certain unlikely scenarios, allow a periodic thread more than its CPU budget in a single period. Such a behaviour can undermine any schedulability analysis that has been undertaken. In this paper, we present a revised formal model, which corrects this anomalous behaviour, and evaluate its properties. We also extend the formal model, so it allows support for real-time threads with sporadic and aperiodic releases, and show how our revised cost enforcement model is valid for all types of threads.

带数据约束实时系统的模型检测

带数据约束的实时系统是指一种既带有时间约束又带有数据变量约束的计算系统。目前将离散数据约束和连续时间约束统一在一个模型中的规范及验证研究较少。文中提出了一种既带有连续数据约束又带有离散数据约束的规范——基于连续时间的ZIA规范,并给出它的时序逻辑。MARTE是UML在嵌入式实时系统领域的建模规范,在工业界的应用非常广泛,但是目前对其模型检测的研究较少。在MARTE的基础上扩展Z,提出了Z-MARTE,并将Z-MARTE转换为基于连续时间的ZIA模型,在实现对连续时间ZIA模型检测的同时,也实现了对Z-MARTE的模型检测。最后通过一个实例进行验证,说明此方法可行有效。     

基于Java内存模型的并发程序模型检测

为了提高性能,Java内存模型允许编译器在优化过程中改变代码的执行顺序,同时该技术也会造成共享数据的更新顺序与本来的执行顺序不同。在多线程Java并发程序中,这些代码乱序执行会引起很多难以发现的错误。现有的Java程序模型检测技术并没有考虑这些顺序改变的问题。因此,本文提出了一种建立包含多线程交互及线程内代码乱序执行的完整模型,并利用模型检测工具进行穷举检测的算法。该算法可以发现原有技术无法发现的新问题,更好地检测高可靠性要求的Java并发程序。     

基于语义约束的数据转换模式研究

XML是因特网中不同企业之间进行信息交流的一种标准的数据转换模式,为了加速数据之间的转换,企业组织通过定义公共数据文档接口来实现基于XML的应用。本文提出了一种新的将关系数据模式转换为XML模式的方法。在转换的过程中,不仅考虑关系模式的结构,而且考虑语义约束,比如内部函数依赖。该方法的输入模式是具有多值函数依赖的关系模式,输出模式是X-Schema。最后,通过实验对该转换方法进行了验证。     

一种支持QoS约束的语义Web服务发现框架

针对当前语义Web服务发现缺乏QoS约束的问题,构建一个支持QoS约束的语义Web服务发现框架。使用QoS认证中心确保QoS信息的动态更新。基于该框架提出一种支持QoS约束的语义Web服务匹配算法,通过实验证明该框架的有效性和可用性。     

Java-MaC: A Run-Time Assurance Approach for Java Programs

We describe Java-MaC, a prototype implementation of the Monitoring and Checking (MaC) architecture for Java programs. The MaC architecture provides assurance that the target program is running correctly with respect to a formal requirements specification by monitoring and checking the execution of the target program at run-time. MaC bridges the gap between formal verification, which ensures the correctness of a design rather than an implementation, and testing, which does not provide formal guarantees about the correctness of the system.Use of formal requirement specifications in run-time monitoring and checking is the salient aspect of the MaC architecture. MaC is a lightweight formal method solution which works as a viable complement to the current heavyweight formal methods. In addition, analysis processes of the architecture including instrumentation of the target program, monitoring, and checking are performed fully automatically without human direction, which increases the accuracy of the analysis. Another important feature of the architecture is the clear separation between monitoring implementation-dependent low-level behaviors and checking high-level behaviors, which allows the reuse of a high-level requirement specification even when the target program implementation changes. Furthermore, this separation makes the architecture modular and allows the flexibility of incorporating third party tools into the architecture. The paper presents an overview of the MaC architecture and a prototype implementation Java-MaC.     

JUTA: 一个Java自动化单元测试工具

描述了一个Java自动化的单元测试工具JUTA.JUTA首先调用工具Soot解析单个Java方法的源码,并将源码解析成一个控制流图.在此基础上,采用符号执行的方法分析控制流图上的路径.工具能够自动地产生满足覆盖率标准的程序的测试用例.这种方法产生的所有测试用例都是可执行的,并且一般来说具有较小的测试用例数.如果用户能够合理地给出描述程序错误的断言,框架JUTA能够自动地检查源码中部分特定类型的错误.实验结果表明工具对Java单元代码的动态测试和静态测试均能在可接受的时间内给出有效的结果.     

Automatic Implication Checking for CHR Constraints

Constraint Handling Rules (CHRs) are a high-level rule-based programming language commonly used to define constraint solvers. We present a method for automatic implication checking between constraints of CHR solvers. Supporting implication is important for implementing extensible solvers and reification, and for building hierarchical CHR constraint solvers. Our method does not copy the entire constraint store, but performs the check in place using a trailing mechanism. The necessary code enhancements can be done by automatic program transformation based on the rules of the solver. We extend our method to work for hierarchically organized modular CHR solvers. We show the soundness of our method and its completeness for a restricted class of canonical solver as well as for specific existing non-canonical CHR solvers. We evaluate our trailing method experimentally by comparing with the copy approach: runtime is almost halved.     

Integrating a formal method into a software engineering process with UML and Java

We describe how CSP-OZ, a formal method combining the process algebra CSP with the specification language Object-Z, can be integrated into an object-oriented software engineering process employing the UML as a modelling and Java as an implementation language. The benefit of this integration lies in the rigour of the formal method, which improves the precision of the constructed models and opens up the possibility of (1) verifying properties of models in the early design phases, and (2) checking adherence of implementations to models. The envisaged application area of our approach is the design of distributed reactive systems. To this end, we propose a specific UML profile for reactive systems. The profile contains facilities for modelling components, their interfaces and interconnections via synchronous/broadcast communication, and the overall architecture of a system. The integration with the formal method proceeds by generating a significant part of the CSP-OZ specification from the initially developed UML model. The formal specification is on the one hand the starting point for verifying properties of the model, for instance by using the FDR model checker. On the other hand, it is the basis for generating contracts for the final implementation. Contracts are written in the Java Modeling Language (JML) complemented by CSP_jassda, an assertion language for specifying orderings between method invocations. A set of tools for runtime checking can be used to supervise the adherence of the final Java implementation to the generated contracts. This research was partially supported by the DFG project ForMooS (grants OL 98/3-2 and WE 2290/5-1). C. B. Jones     

Java 技术框架概述

从体系结构的角度分析了目前流行的java技术框架,详细阐述了java技术体系结构的各主要组成部分。对目前流行的java社区的各种技术进行了说明,并对java技术的发展趋势进行了分析。     

基于可靠词汇语义约束的词语向量表达修正研究

词语向量表达(word vector representation)是众多自然语言处理(natural language processing,NLP)下游应用的基础。已有研究采用各种词汇分类体系提供的词汇语义约束,对海量语料训练得到的词向量进行修正,改善了词向量的语义表达能力。然而,人工编制或者半自动构建的词汇分类体系普遍存在语义约束可靠性不稳定的问题。该文基于词汇分类体系与词向量之间、以及异构词汇分类体系之间的交互确认,研究适用于词语向量表达修正的可靠词汇语义约束提炼方法。具体上,对于词汇分类体系提供的同义词语类,基于词语向量计算和评估类内词语的可靠性。在其基础上,通过剔除不可靠语义约束机制避免词语类划分潜在不够准确的词语的错误修正;通过不同词汇分类体系的交互确认恢复了部分误剔除的语义约束;并通过核心词约束传递机制避免原始词向量不够可靠的词语在词向量修正中的不良影响。该文采用NLPCC-ICCPOL 2016词语相似度测评比赛中的PKU 500数据集进行测评。在该数据集上,将该文提出的方法提炼的可靠词汇语义约束应用到两个轻量级后修正的研究进展方法,修正后的词向量都获得更好的词语相似度计算性能,取得了0.649 7的Spearman等级相关系数,比NLPCC-ICCPOL 2016词语相似度测评比赛第一名的方法的结果提高25.4%。     

Java动态代理的研究与应用

Java动态代理机制的出现,使得Java开发人员不用手工编写代理类,只要简单地指定一组接口及委托类对象,便能动态地获得代理类。代理类会负责将所有的方法调用分派到委托对象上反射执行,在分派执行的过程中,开发人员还可以按需调整委托类对象及其功能,这是一套非常灵活有弹性的代理框架。针对此框架的优点,把它引入到考试系统的应用中,使得系统的维护和扩展增强,而且减少了编程工作量。     

基于装配约束动态管理的虚拟拆卸

装配约束是虚拟拆卸环境下必须考虑的装配体的重要信息，提出虚拟拆卸过程中装配约束的动态管理机制，并实现了基于装配约束导航的虚拟拆卸。装配约束的动态管理包括虚拟环境下装配约束的获取、表达以及拆卸过程中装配约束的动态维护，即装配约束的动态解除和产生，文中用装配约束图表达零件间的装配约束，提出装配约束的间接解除方法，并实现了基于装配约束推理的零件可拆卸方向的推导。最后，通过一个简单装配体的拆卸实例，对文中方法进行了验证。     

面向Java锁机制的字节码自动重构框架

Java语言提供了同步锁、可重入锁和读写锁等几种锁机制,在并行程序设计中不同的数据结构使用这几种锁机制时获得的性能通常是不同的。为了在不同的锁机制之间进行自动转换,进而帮助程序员了解程序的性能,提出了一种面向Java锁机制的字节码自动重构框架,并基于该框架实现了字节码重构工具Lock2Lock。Lock2Lock在Quad中间表示的基础上对字节码进行静态分析,并对分析的结果进行一致性验证,通过Javassist完成字节码的重构。使用红黑树、消费者生产者程序以及SPECjbb2005 3个测试程序对Lock2Lock重构工具进行了测试,结果表明,Lock2Lock可以成功地实现从同步锁到可重入锁或读写锁的重构。     

Improving the official specification of Java bytecode verification

Bytecode verification is the main mechanism to ensure type safety in the Java Virtual Machine. Inadequacies in its official specification may lead to incorrect implementations where security can be broken and/or certain legal programs are rejected. This paper provides a comprehensive analysis of the specification, along with concrete suggestions for improvement. Copyright © 2003 John Wiley & Sons, Ltd.     

基于Web数据库动态访问技术的Java实现

对基于Ｂｒｏｗｓｅｒ／Ｓｅｒｖｅｒ模式下的Ｉｎｔｒａｎｅｔ网的几种Ｗｅｂ动态访问技术进行了分析,讨论了这几种技术的优缺点,详细论述了ＪａｖａＳｅｒｖｌｅｔ、Ｊａｖａ、Ａｐｐｌｅｔ与ＪＤＢＣ相结合的技术,并就这一方案进行了改进,使用了一我层体系工将将其应用实际的Ｉｎｔｒａｎｅｔ的Ｗｅｂ开发实践中去。     

一种用于硬实时Java处理器的类转换器设计及实现

通过分析Class文件处理过程及其中影响实时性的操作，提出一种用于硬实时Java处理器的类转换器，它读取标准Class文件，处理并生成适合Java处理器直接执行的内存映像文件．由于装载、连接过程中大量操作（如符号引用的解析）都由类转换器提前处理完毕，使得Java处理器操作大为简化．同时，由于所有影响Java处理器实时性的操作也由类转换器提前处理，Java处理器最坏情况执行时间（Worst Case Execution Time）完全可预测．     

Checking Event-Based Specifications in Java Systems

One of today's challenges is producing reliable software in the face of an increasing number of interacting components. Our system CHET lets developers define specifications describing how a component should be used and checks these specifications in real Java systems. CHET is able to check a wide range of complex conditions in large software systems without programmer intervention. It does this by doing a complete and detailed flow analysis of the software and using this analysis to build a simpler, model program. This paper explores the motivations for CHET, the specification techniques that are used, and the methodology used in statically checking that the specifications are obeyed in a system.