Modeling and visualizing object-oriented programs with Codecharts

Software design, development and evolution commonly require programmers to model design decisions, visualize implemented programs, and detect conflicts between design and implementation. However, common design notations rarely reconcile theoretical concerns for rigor and minimality with the practical concerns for abstraction, scalability and automated verifiability. The language of Codecharts was designed to overcome these challenges by narrowing its scope to visual specifications that articulate automatically-verifiable statements about the structure and organization of object-oriented programs. The tokens in its visual vocabulary stand for the building-blocks of object-oriented design, such as inheritance class hierarchies, sets of dynamically-bound methods, and their correlations. The formalism was tailored for those pragmatic concerns which arise from modeling class libraries and design patterns, and for visualizing programs of any size at any level of abstraction. We describe design verification, a process of proving or refuting that a Java program (i.e. its native code) conforms to the Codechart specifying it. We also describe a toolkit which supports modeling and visualization with Codecharts, as well as a fully-automated design verification tool. We conclude with empirical results which suggest gains in both speed and accuracy when using Codecharts in software design, development and evolution.     

Principles to Support Modular Software Construction

The construction of large software systems is always achieved through assembly of independently written components — program modules. For these software components to work together, they must share a common set of data types and principles for representing structured data such as arrays of values and files. This common set of tools for creating and operating on data objects is provided by the infrastructure of the computer system: the hardware, operating system and runtime code. Because the nature and properties of these tools are crucial for correct operation of software components and their inter-operation, it is essential to have a precise specification that may be used for verifying correctness of application software on one hand, and to verify correctness of system behavior on the other. We call such a specification a program execution model (PXM). It is evident that the properties of the PXM implemented by a computer system can have serious impact on the ability of application programmers to practice modular software construction. This paper discusses the concept of program execution models and presents a set of principles that a PXM must satisfy to provide a sound basis for modular software construction. Because parallel program execution on computer systems with many processing units is an essential part of contemporary computing environments, the expression of parallelism and modular software construction using components involving parallel operations is included in this treatment. The conclusion is that it is possible to build computer systems that implement a PXM within which any parallel program may be used, unmodified, as a component for building more substantial parallel programs.     

The analysis of architectural languages for the needs of practitioners

Architectural languages (ALs) have attracted much attention as the modeling notations for specifying and reasoning about important design decisions. In this study, 124 different existing ALs have been analyzed for a set of requirements that are crucial for practitioners. These requirements are concerned with language definition, language features, and tool support. Some of the important findings obtained from the analysis are as follows: (1) performance is the top popular nonfunctional requirement supported by ALs; (2) no ALs offer both textual and visual notation sets, one of which could be used independently; (3) process algebras are the top preferred formal method by formal ALs; (4) the physical, deployment, and operational viewpoints are rarely supported by ALs; (5) the top preferred extension mechanism of the extensible ALs is XML for syntax extension; (6) Java is the top preferred programming language in generating software code; (7) the exhaustive model checking is the top preferred automated analysis method; (8) the logic‐based formal techniques are so popular in specifying system requirements; (9) among the analysis properties considered, consistency is the top supported property for the automated checking; and (10) most ALs do not provide any discussion platform (eg, forums). Hence, these findings can be used by the new AL developers in addressing the needs of practitioners and bridging the gaps in the field. Practitioners can also use the findings to find out about the existing ALs and compare them to choose the one(s) that suits their needs best.     

A formal verification framework for static analysis

Static analysis tools, such as resource analyzers, give useful information on software systems, especially in real-time and safety-critical applications. Therefore, the question of the reliability of the obtained results is highly important. State-of-the-art static analyzers typically combine a range of complex techniques, make use of external tools, and evolve quickly. To formally verify such systems is not a realistic option. In this work, we propose a different approach whereby, instead of the tools, we formally verify the results of the tools. The central idea of such a formal verification framework for static analysis is the method-wise translation of the information about a program gathered during its static analysis into specification contracts that contain enough information for them to be verified automatically. We instantiate this framework with costa, a state-of-the-art static analysis system for sequential Java programs, for producing resource guarantees and KeY, a state-of-the-art verification tool, for formally verifying the correctness of such resource guarantees. Resource guarantees allow to be certain that programs will run within the indicated amount of resources, which may refer to memory consumption, number of instructions executed, etc. Our results show that the proposed tool cooperation can be used for automatically producing verified resource guarantees.     

A decision procedure for detecting atomicity violations for communicating processes with locks

The problem of interest is to verify data consistency of a concurrent Java program. In particular, we present a new decision procedure for verifying that a class of data races caused by inconsistent accesses on multiple fields of an object cannot occur (so-called atomic-set serializability). Atomic-set serializability generalizes the ordinary notion of a data race (i.e., inconsistent coordination of accesses on a single memory location) to a broader class of races that involve accesses on multiple memory locations. Previous work by some of the authors presented a technique to abstract a concurrent Java program into an EML program, a modeling language based on pushdown systems and a finite set of reentrant locks. Our previous work used only a semi-decision procedure, and hence provides a definite answer only some of the time. In this paper, we rectify this shortcoming by developing a decision procedure for verifying data consistency, i.e., atomic-set serializability, of an EML program. When coupled with the previous work, it provides a decision procedure for verifying data consistency of a concurrent Java program. We implemented the decision procedure, and applied it to detect both single-location and multi-location data races in models of concurrent Java programs. Compared with the prior method based on a semi-decision procedure, not only was the decision procedure 34 times faster overall, but the semi-decision procedure timed out on about 50% of the queries, whereas the decision procedure timed out on none of the queries.     

Generative software product line development using variability-aware design patterns

Software Product Lines (SPLs) are an approach to reuse in-the-large that models a set of closely related software systems in terms of commonalities and variabilities. Design patterns are best practices for addressing recurring design problems in object-oriented source code. In the practice of implementing SPL, instances of certain design patterns are employed to handle variability, which makes these “variability-aware design patterns” a best practice for SPL design. However, currently there is no dedicated method for proactively developing SPLs using design patterns suitable for realizing variable functionality. In this paper, we present a method to perform generative SPL development with design patterns. We use role models to capture design patterns and their relation to a variability model. We further allow mapping of individual design pattern roles to (parts of) implementation elements to be generated (e.g., classes, methods) and check the conformance of the realization with the specification of the pattern. We provide definitions for the variability-aware versions of the design patterns Observer, Strategy, Template Method and Composite. Furthermore, we support generation of realizations in Java, C++ and UML class diagrams utilizing annotative, compositional and transformational variability realization mechanisms. Hence, we support proactive development of SPLs using design patterns to apply best practices for the realization of variability. We realize our concepts within the Eclipse IDE and demonstrate them within a case study.     

Ann: A domain-specific language for the effective design and validation of Java annotations

This paper describes a new modelling language for the effective design and validation of Java annotations. Since their inclusion in the 5th edition of Java, annotations have grown from a useful tool for the addition of meta-data to play a central role in many popular software projects. Usually they are not conceived in isolation, but in groups, with dependency and integrity constraints between them. However, the native support provided by Java for expressing this design is very limited.To overcome its deficiencies and make explicit the rich conceptual model which lies behind a set of annotations, we propose a domain-specific modelling language. The proposal has been implemented as an Eclipse plug-in, including an editor and an integrated code generator that synthesises annotation processors. The environment also integrates a model finder, able to detect unsatisfiable constraints between different annotations, and to provide examples of correct annotation usages for validation. The language has been tested using a real set of annotations from the Java Persistence API (JPA). Within this subset we have found enough rich semantics expressible with Ann and omitted nowadays by the Java language, which shows the benefits of Ann in a relevant field of application.     

As-if-serial exception handling semantics for Java futures

Exception handling enables programmers to specify the behavior of a program when an exceptional event occurs at runtime. Exception handling, thus, facilitates software fault tolerance and the production of reliable and robust software systems. With the recent emergence of multi-processor systems and parallel programming constructs, techniques are needed that provide exception handling support in these environments that are intuitive and easy to use. Unfortunately, extant semantics of exception handling for concurrent settings is significantly more complex to reason about than their serial counterparts.In this paper, we investigate a similarly intuitive semantics for exception handling for the future parallel programming construct in Java. Futures are used by programmers to identify potentially asynchronous computations and to introduce parallelism into sequential programs. The intent of futures is to provide some performance benefits through the use of method-level concurrency while maintaining as-if-serial semantics that novice programmers can easily understand — the semantics of a program with futures is the same as that for an equivalent serial version of the program. We extend this model to provide as-if-serial exception handling semantics. Using this model our runtime delivers exceptions to the same point it would deliver them if the program was executed sequentially. We present the design and implementation of our approach and evaluate its efficiency using an open source Java virtual machine.     

Semantic interoperability in building design: Methods and tools

Semantic interoperability is a crucial element to make building information models understandable and model data sharable across multiple design disciplines and heterogeneous computer systems. This paper presents a new approach and its software implementation for the development of building design objects with semantics of interoperable information to support semantic interoperability in building designs. The novelty of the approach includes its incorporation of building design domain ontology, object-based CAD information modeling, and interoperability standard to make building information models and model data semantically interoperable. A set of methods are proposed to address the issues of object-based building information representation compliant with the Industrial Foundation Classes (IFC); extension of IFC models with the supplementary information; and semantic annotation of the interoperable and extensible information sets. The prototype implementation of these methods provides a set of Web-enabled software tools for effectively generating, managing, and reusing the semantically interoperable building objects in design applications of architectural CAD, structural analysis, and building code conformance checking.     

Scaling step-wise refinement

Step-wise refinement is a powerful paradigm for developing a complex program from a simple program by adding features incrementally. We present the AHEAD (algebraic hierarchical equations for application design) model that shows how step-wise refinement scales to synthesize multiple programs and multiple noncode representations. AHEAD shows that software can have an elegant, hierarchical mathematical structure that is expressible as nested sets of equations. We review a tool set that supports AHEAD. As a demonstration of its viability, we have bootstrapped AHEAD tools from equational specifications, refining Java and nonJava artifacts automatically; a task that was accomplished only by ad hoc means previously.     

Statically safe program generation with SafeGen

SafeGen is a meta-programming language for writing statically safe generators of Java programs. If a program generator written in SafeGen passes the checks of the SafeGen compiler, then the generator will only generate well-formed Java programs, for any generator input. In other words, statically checking the generator guarantees the correctness of any generated program, with respect to static checks commonly performed by a conventional compiler (including type safety, existence of a superclass, etc.). To achieve this guarantee, SafeGen supports only language primitives for reflection over an existing well-formed Java program, primitives for creating program fragments, and a restricted set of constructs for iteration, conditional actions, and name generation. SafeGen’s static checking algorithm is a combination of traditional type checking for Java, and a series of calls to a theorem prover to check the validity of first-order logical sentences, constructed to represent well-formedness properties of the generated program under all inputs. The approach has worked quite well in our tests, providing proofs for correct generators or pointing out interesting bugs.     

The accuracy of dependency analysis in static architecture compliance checking

Architecture compliance checking (ACC) is an approach to verify conformance of implemented program code to high‐level models of architectural design. Static ACC focuses on the modular software architecture and on the existence of rule violating dependencies between modules. Accurate tool support is essential for effective and efficient ACC. This paper presents a study on the accuracy of ACC tools regarding dependency analysis and violation reporting. Ten tools were tested and compared by means of a custom‐made benchmark. The Java code of the benchmark testware contains 34 different types of dependencies, which are based on an inventory of dependency types in object oriented program code. In a second test, the code of open source system FreeMind was used to compare the 10 tools on the number of reported rule violating dependencies and the exactness of the dependency and violation messages. On the average, 77% of the dependencies in our custom‐made test software were reported, while 72% of the dependencies within a module of FreeMind were reported. The results show that all tools in the test could improve the accuracy of the reported dependencies and violations, though large differences between the 10 tools were observed. We have identified 10 hard‐to‐detect types of dependencies and four challenges in dependency detection. The relevance of our findings is substantiated by means of a frequency analysis of the hard‐to‐detect types of dependencies in five open source systems. © 2016 The Authors. Software: Practice and Experience Published by John Wiley & Sons, Ltd.     

基于WWW的仿真软件JRTSS

基于ＷＷＷ的仿真软件ＪＲＴＳＳ（Ｊａｖａ－ｂａｓｅｄＲｅａｌＴｉｍｅＳｙｓｔｅｍＳｉｍｕｌａｔｏｒ）以ＲＴＳＳ仿真软件为基础,保持其原有特色,并采用Ｊａｖａ为编程语言,运行在Ｂｒｏｗｓｅｒ／Ｓｅｒｖｅｒ环境下。ＪＲＴＳＳ软件由三部分组成：仿真核心、建模程序与结果后处理程序。其中仿真核心运行在Ｓｅｒｖｅｒ端,建模和结果后处理程序为ＪａｖａＡｐｐｌｅｔ,由用户的Ｂｒｏｗｓｅｒ下载并执行。ＪＲＴＳＳ的系统模型是一个开放队列网络。通过在不同抽象层次对多个数据采集与处理系统、通信网络以及柔性制造系统的仿真与性能评价,证实ＪＲＴＳＳ是一个用于系统开发的有力工具。     

在Java中使用契约式设计

契约式设计DBC是面向对象程序设计的一项技术，其目的在于提高软件的质量、可靠性与可复用性。Java语言本身还不直接支持契约式设计，但借助一些外部辅助工具可以使该项技术获得应用。对此，给出了两种实现方法：一种是使用预编译器；另一种是使用面向方面的程序设计技术。     

Developing Java applications for a nuclear fusion experiment: a test case for Java applicability in a demanding environment

The paper describes the experience gained in the development of Java applications in a nuclear fusion experiment. Two Java tools for graphical data display and experiment configuration set‐up are presented as case studies. Based on these tools, the results derived by the application of some metrics for object oriented software and by the analysis of the design patterns imported in the applications are presented to highlight the effective code reuse achieved with Java. The main issues in the applicability of Java in a demanding environment are then introduced and a few weaknesses of the language are finally discussed. Copyright © 2001 John Wiley & Sons, Ltd.     

基于Rebeca模型的硬件设计形式化验证

形式化验证是对传统验证方法的补充,是数字电路验证的一条有效途径,对于并发系统,行为建模是一种非常合适的建模方法;Rebeca是由Sirjani和Movaghar提出的一种基于行为的建模语言,支持形式化,一方面,Rebeca是一种类Java的语言,软件工程师很容易使用,另一方面,它是一种支持形式化验证及其相关理论的模型语言,可以为不精通于形式化方法的开发人员和研究人员提供方便的验证过程;在深入研究Rebeca的基础上,采用Rebeca对硬件设计进行建模,然后Modere形式化验证工具对AES密码芯片进行形式化验证。