Summary This paper presents the motivation for and outcomes of an engineering research project on certifiable Java for embedded systems. The project supports the upcoming standard for safety‐critical Java, which defines a subset of Java and libraries aiming for development of high criticality systems. The outcome of this project include prototype safety‐critical Java implementations, a time‐predictable Java processor, analysis tools for memory safety, and example applications to explore the usability of safety‐critical Java for this application area. The text summarizes developments and key contributions and concludes with the lessons learned. Copyright © 2016 John Wiley & Sons, Ltd.

Summary In order to claim conformance with a Java Specification Request, a Java implementation has to pass all tests in an associated Technology Compatibility Kit. This paper presents a model‐based development of a Technology Compatibility Kit test suite and a test execution tool for the draft safety‐critical Java profile specification. The Java Modeling Language is used to model conformance constraints for the profile. Java Modeling Language annotations define contracts for classes and interfaces. The annotations are translated by a tool into runtime assertion checks. Hereby, the design and elaboration of the concrete test cases are simplified, because the expected results are derived from contracts and thus do not need to be provided explicitly. Bottom‐up testing is applied for testing methods of the safety‐critical Java classes, whereas top‐down testing is applied for testing global properties, such as protocols, memory management, and real‐time properties, including scheduling. The tests are executed using a simplified version of JUnit, which makes the test suite executable on resource‐constrained platforms. Copyright © 2017 John Wiley & Sons, Ltd.

SUMMARY The Java programming language was originally developed for embedded systems, but the resource requirements of previous and current Java implementations – especially memory consumption – tend to exclude them from being used on a significant class of resource constrained embedded platforms. The contribution of this paper is an architecture and implementation of a Java execution stack for resource constrained embedded platforms with a few kB of RAM and flash memory. The resource requirements of the presented architecture has been reduced significantly through all the layers of the architecture by integrating the following: (1) a lean virtual machine without any external dependencies on POSIX‐like libraries or other OS functionalities; (2) a hardware abstraction layer, implemented almost entirely in Java through the use of hardware objects, first level interrupt handlers, and native variables; and (3) an implementation of the Safety‐Critical Java profile Level 0 and 1 for hard real‐time applications. All Java components of a given application are minimized through program specialization, and because (2) and (3) are written in Java, the program specialization has a significant impact on the resulting program size. An evaluation of the presented solution shows that the miniCDj benchmark gets reduced to a size where it can run on resource constrained platforms. Copyright © 2013 John Wiley & Sons, Ltd.

TEST 02 - Elsevier's Scopus, the largest abstract and citation database of peer-reviewed literature. Search and access research from the science, technology, medicine, social sciences and arts and humanities fields.

SUMMARY Chip‐multiprocessors offer increased processing power at a low cost. However, in order to use them for real‐time systems, tasks have to be scheduled efficiently and predictably. It is well known that finding optimal schedules is a computationally hard problem. In this paper we present a solution that uses model checking to find a static schedule, if one exists at all, which gives an implementation of a table driven multiprocessor scheduler. Mutual exclusion to access shared resources is guaranteed by including access constraints in the schedule generation. To evaluate the proposed cyclic executive for multiprocessors, we have implemented it in the context of safety‐critical Java on a Java processor. Copyright © 2011 John Wiley & Sons, Ltd.

Just like other software, Java profiles benefits from refactoring when they have been used and have evolved for some time. This paper presents a refactoring of the Real-Time Specification for Java (RTSJ) and the Safety Critical Java (SCJ) profile (JSR-302). It highlights core concepts and makes it a suitable foundation for the proposed levels of SCJ. The ongoing work of specifying the SCJ profile builds on sub classing of RTSJ. This spurred our interest in a refactoring approach. It starts by extracting the common kernel of the specifications in a core package, which defines interfaces only. It is then possible to refactor SCJ with its three levels and RTSJ in such a way that each profile is in a separate package. This refactoring results in cleaner class hierarchies with no superfluous methods, well defined SCJ levels, elimination of SCJ annotations like @SCJAllowed, thus making the profiles easier to comprehend and use for application developers and students.

Embedded systems use specialized hardware devices to interact with their environment, and since they have to be dependable, it is attractive to use a modern, type-safe programming language like Java to develop programs for them. Standard Java, as a platform-independent language, delegates access to devices, direct memory access, and interrupt handling to some underlying operating system or kernel, but in the embedded systems domain resources are scarce and a Java Virtual Machine (JVM) without an underlying middleware is an attractive architecture. The contribution of this article is a proposal for Java packages with hardware objects and interrupt handlers that interface to such a JVM. We provide implementations of the proposal directly in hardware, as extensions of standard interpreters, and finally with an operating system middleware. The latter solution is mainly seen as a migration path allowing Java programs to coexist with legacy system components. An important aspect of the proposal is that it is compatible with the Real-Time Specification for Java (RTSJ).

Models of embedded systems with communicating actors and deadlines offer abstraction and encapsulation of related functionality, but their behavior is complex. Verification is therefore difficult and requires a combination of simulation, model checking and testing tools. In order to rely on the results, these tools must use consistent semantics for the model. Yet, a monolithic semantic model is just as complex as the entity it describes. In order to circumvent this issue, we define a three level semantics giving independent definitions of the functionality of actors, the temporal properties of communications, and finally imposing deadlines on the timing of dependent actors. With this approach the semantics is used directly in developing a simulator supporting the nondeterminism of the abstract semantics such that e.g. potential race conditions can be detected. The layers are also planned to underpin independent specialized verification tools. The verification task for timed, hybrid systems can thus be divided into the continuous, discrete, and timing domains with automated translation to specialized tools, and this promises better scalability than simulation or model checking of one complex model.

There are numerous existing notations and standards in the Web service community. These may be grouped broadly into three competing families, namely; Web services, semantic Web, and electronic business. Although the families are competing, we expect that applications will cut across them and there is a need to map from one to another and to analyze compatibility and other properties. Therefore we survey how they deal with different aspects. We then illustrate with examples, the aspects of contracts captured by one language from each of the three competing families in addition to WSDL, the core standard for Web services description. The result is a classification based on the aspects of computations: functionality, protocol, and for instance performance covered by the languages. The classification is used to identify similarities between semantic models and thus find potential mappings between the families. Furthermore, this gives a handle on analysis techniques that may apply to the aspects in a particular family.

An important part of implementing device drivers is to control the interrupt facilities of the hardware platform and to program interrupt handlers. Current methods for handling interrupts in Java use a server thread waiting for the VM to signal an interrupt occurrence. It means that the interrupt is handled at a later time, which has some disadvantages. We present constructs that allow interrupts to be handled directly and not at a later point decided by a scheduler. A desirable feature of our approach is that we do not require a native middelware layer but can handle interrupts entirely with Java code. We have implemented our approach using an interpreter and a Java processor, and give an example demonstrating its use.

Java, as a safe and platform independent language, avoids access to low-level I/O devices or direct memory access. In standard Java, low-level I/O is not a concern; it is handled by the operating system. However, in the embedded domain resources are scarce and a Java virtual machine (JVM) without an underlying middleware is an attractive architecture. When running the JVM on bare metal, we need access to I/O devices from Java; therefore we investigate a safe and efficient mechanism to represent I/O devices as first class Java objects, where device registers are represented by object fields. Access to those registers is safe as Java's type system regulates it. The access is also fast as it is directly performed by the bytecodesgetfield and putfield. Hardware objects thus provide an object-oriented abstraction of low-level hardware devices. As a proof of concept, we have implemented hardware objects in three quite different JVMs: in the Java processor JOP, the JIT compiler CACAO, and in the interpreting embedded JVM SimpleRTJ.

Modern software applications ranging from enterprise to embedded systems are becoming increasingly complex, and require very high levels of dependability assurance. The most effective means to handle complexity is separation of concerns and incremental development, and assurance of dependability requires formal methods. We report here our experience on these issues in an application of a formal calculus, rCOS, to a component-based design of the point of sale system (POS). We demonstrate the possibility in scaling-up correctness by design and discuss how rCOS may be integrated with current and emerging software engineering tools.

We propose a new, minimal specification for real-time Java for safety critical applications. The intention is to provide a profile that supports programming of applications that can be validated against safety critical standards such as DO-178B (1992). The proposed profile is in line with the Java specification request JSR-302: Safety Critical Java Technology, which is still under discussion. In contrast to the current direction of the expert group for the JSR-302 we do not subset the rather complex Real-Time Specification for Java (RTSJ). Nevertheless, our profile can be implemented on top of an RTSJ compliant JVM

Software development tools need to support more and more phases of the entire development process, because applications must be developed more correctly and efficiently. The tools therefore need to integrate sophisticated checkers, generators and transformations. A feasible approach to ensure high quality of such add-ins is to base them on sound formal foundations. In order to know where such add-ins will fit, we investigate the use of an existing successful commercial tool and identify suitable places for adding formally supported checking, transformation and generation modules. The paper concludes with a discussion of feasibility of developing the proposed add-ins and how to give conditions such that they will actually be used.

Abstract. Linear temporal logic (LTL) has been widely used for specification and verification of reactive systems. Its standard model is sequences of states (or state transitions), and formulas describe sequencing of state transitions. When LTL is used to model real-time systems, a state is extended with a time stamp to record when a state transition takes place. Duration calculus (DC) is another well studied approach for real-time systems development. DC models behaviours of a system by functions from the domain of reals representing time to the system states. This paper extends this time domain to the Cartesian product of the real and the natural numbers. With the extended time domain, we provide the chop modality with a non-overlapping interpretation. This allows some linear temporal operators explicitly dealing with the discrete dimension of time to be derivable from the chop modality in essentially the same way that their continuous-time counterparts are in the classical DC. This provides a nice embedding of some timed LTL (TLTL) modalities into DC to unify the methods from DC and LTL for real-time systems development: Requirements and high level design decisions are interval properties and are therefore specified and reasoned about in DC, while properties of an implementation, as well as the refinement relation between two implementations, are specified and verified compositionally and inductively in LTL. Implementation properties are related to requirement and design properties by rules for lifting LTL formulas to DC formulas.

Software for safety critical systems must deal with the hazards identified by safety analysis. This paper investigates, how the results of one safety analysis technique, fault trees, are interpreted as software safety requirements to be used in the program design process. We propose that fault tree analysis and program development use the same system model. This model is formalized in a real-time, interval logic, based on a conventional dynamic systems model with state evolving over time. Fault trees are interpreted as temporal formulas, and it is shown how such formulas can be used for deriving safety requirements for software components.

An approach to specification of requirements and verification of design for real-time systems is presented. A system is defined by a conventional mathematical model for a dynamic system where application specific states denote functions of real time. Specifications are formulas in duration calculus, a real-time interval logic, where predicates define durations of states. Requirements define safety and functionality constraints on the system or a component. A top-level design is given by a control law: a predicate that defines an automation controlling the transition between phases of operation. Each phase maintains certain relations among the system states; this is analogous to the control functions known from conventional control theory. The top-level design is decomposed into an architecture for a distributed system with specifications for sensor, actuator, and program components. Programs control the distributed computation through synchronous events. Sensors and actuators relate events with system states. Verification is a deduction showing that a design implies requirements.>

This paper investigates the desirable properties of programming language constructs that support encapsulation of environments and abstract data types.These properties are illustrated by using a simple multiuser file system as a model.The requirements for such a file system are outlined; then the model file system design is described by a hierarchy of encapsulated abstract data types and environments.The high-level language constructs necessary to directly implement the model file system design are identified.It is concluded that environment encapsulation and abstract data types must be supported by different constructs, and the desirable properties of such constructs are outlined.A superset of Ada e that effectively supports both environments and abstract data types is introduced and used to implement the model file system.The encapsulation constructs of several modern systems programming languages are evaluated.Each of these languages is shown to be insufficient for a direct implementation of the model file system design.

Abstract Concurrent Pascal and similar languages are inefficient when used to program systems where processes exchange large messages. The inefficiencies, caused by copying of data, can be removed by introducing pointer variables, and this paper shows how this is done without allowing unrestricted sharing of variables. Pointer variables also give means to solve problems of dynamic resource allocation and dynamic addressing. Examples with performance figures for an actual implementation are given.

A driver is the part of an I/O system used for processing of an I/O request for a specific channel. The interaction of the CPU with a channel is described through the monitor concept of Hoare and Brinch Hansen. The implementation of monitors using hardware interrupt facilities is described. The resulting device monitor is compared pared with the device processes of Wirth's Modula. The concept is illustrated through an extension to Concurrent Pascal with examples drawn from the PDP11 system. Problems of missing interrupts and power failure are also discussed.

Abstract Mutual exclusion and general synchronization of concurrent processes (‘tasks’) are well‐known principles for constructing reliable real‐time systems. This paper shows how to implement these principles under a typical commercial operating system which provides incomplete synchronization operations. The problem of synchronizing erroneous tasks is discussed briefly.