Narrow Results

Research on real-time systems now focuses on formal approaches to specify and analyze the behavior of real-time systems. Temporal logic is a natural candidate for this since it can specify properties of event and state sequences. However, “pure” temporal logic cannot specify “quantitative” aspect of time. The concepts of eventuality, fairness, etc. are essentially “qualitative” treatment of time. The pure temporal logic makes no reference to absolute time. For real-time systems, the pure qualitative specification and analysis of time are inadequate. In this paper, we present a modification of temporal logic—Event-based Real-time Logic (ERL), based on our event-based conceptual model. The ERL provides a high-level framework for specifying timing properties of real-time systems, and it can be implemented using Prolog programming language. In our approach to testing and debugging of real-time systems, the ERL is used to specify both expected behavior (specification) and actual behavior (execution traces) of the target system and to verify that the target system achieves the specification. In this paper, a method is presented to implement the ERL using Prolog programming language for testing and debugging real-time systems.

This paper presents design and performance of a prototype of new humanoid arm that has been developed at the LARM2 laboratory of the University of Rome “Tor Vergata”. This new arm, called LARMbot PK arm, is an upper limb that is designed for the LARMbot humanoid robot. LARMbot is a humanoid robot designed to move freely in open spaces, and able to adapt to task environment. Its objective is to transport objects weighing a few kilograms in order to facilitate the restocking of workstations, or to manage small warehouses and other tasks feasible for humanoids. The LARMbot PK arm is conceived as a solution that is designed on the basis of a parallel tripod structure using linear actuators to provide high agility of movement. This solution is designed with components that can be found on the market or can be created by 3D printing in order to offer a quality and price ratio well convenient for user-oriented humanoid robots. Experimental tests are discussed with the built prototype to demonstrate the capabilities of the proposed solution in terms of agility, autonomy, and power to validate the LARMbot PK arm solution as a satisfactory solution for the new upper limbs of the LARMbot humanoid robot.

This chapter complements the chapters on technical reviews and software reliability engineering in Vol. 1 of the handbook. It is primarily concerned with the verification of code by means of testing, but an example of an informal proof of a program is also given. A practitioner's view of testing is taken throughout, including an overview of how testing is done at Microsoft.

The concept of Visual Routine is introduced. A. description is given of an implemented computer system which can correctly compute in images of simple 2-D geometric shapes eleven common properties and relations. A visual routine programming language is outlined. Issues relevant to the control of visual-routine-based search are discussed. The results of testing the system are reported…