Modular machine tools: Design and barriers to industrial implementation

The Reconfigurable Manufacturing System (RMS) paradigm has been developed to address challenges in the design of manufacturing systems and equipment that will meet the demands of modern manufacturing. This research involved the development of Modular Reconfigurable Machines (MRMs); as an emerging technology in reconfigurable manufacturing. MRMs are mechanically modular machines. The modularity permits the kinematic architecture and processing functions of the machine to be reconfigured to meet changing production requirements. This paper will focus on aspects of the mechanical design and the development of a control system that supported the modularity and reconfigurability of the mechanical platform. A modular electronic system is presented that is characterized by a plug and play approach to control scalability. This is complemented by a software architecture that has been developed with a focus on hardware abstraction for the management of an augmented mechanical and electronic architecture. The implications of MRMs for RMSs are discussed and key inhibitors to industrial implementation are identified.     

A comparison of tools for teaching formal software verification

We compare four tools regarding their suitability for teaching formal software verification, namely the Frege Program Prover, the Key system, Perfect Developer, and the Prototype Verification System (PVS). We evaluate them on a suite of small programs, which are typical of courses dealing with Hoare-style verification, weakest preconditions, or dynamic logic. Finally we report our experiences with using Perfect Developer in class.     

A unified formal basis for the CASE tools system

XYZ system is a CASE tools system based on a temporal logic language XYZ/E which can represent every essential feature of conventional HLL's (sequential or concurrent), specifications of different levels, production rules, operational semantics of graphic languages in a uniform framework. With this formal language as the common basis, all the CASE tools including various kinds of graphic tools for distributed process, concurrent programs with phased memory and sequential programs, tools for verification, rapid-prototyping, language transformation, and module management can be connected freely to form more sophisticated and integrated systems.     

Formal methods and tools for industrial critical systems

International Journal on Software Tools for Technology Transfer - Formal methods and tools have become well established and widely applied to ensure the correctness of fundamental components of...     

Formal methods and tools for industrial critical systems

International Journal on Software Tools for Technology Transfer - Formal methods and tools have become well established and widely applied to ensure the correctness of fundamental components of...     

SOFL: a formal engineering methodology for industrial applications

Formal methods have yet to achieve wide industrial acceptance for several reasons. They are not well integrated into established industrial software processes, their application requires significant abstraction and mathematical skills, and existing tools do not satisfactorily support the entire formal software development process. We have proposed a language called SOFL (Structured-Object-based-formal Language) and a SOFL methodology for system development that attempts to address these problems using an integration of formal methods, structured methods and object oriented methodology. Construction of a system uses structured methods in requirements analysis and specifications, and an object based methodology during design and implementation stages, with formal methods applied throughout the development in a manner that best suits their capabilities. The paper describes the SOFL methodology, which introduces some substantial changes from current formal methods practice. A comprehensive, practical case study of an actual industrial Residential Suites Management System illustrates how SOFL is used     

形式化方法与工具专刊前言

形式化方法是指有严格数学基础的软件和系统开发方法,支持计算机系统及软件的规约、设计、验证与演化等活动.随着高可信软件的兴起,形式化方法作为重要的途径,关注度日益提高.其作用不仅深化了人们对计算系统规律的认识,而且支持了计算系统开发、运行和演化之工具、平台、环境的构建.本专刊收录的11篇论文反映了近年来我国学者在形式化方法与工具领域的部分研究成果.     

VSE: formal methods meet industrial needs

The Verification Support Environment (VSE) is a tool to formally specify and verify complex systems. It provides the means to structure specifications and supports the development process from the specification of a system to the automatic generation of code. Formal developments following the VSE method are stored and maintained in an administration system that guides the user and maintains a consistent state of development. An integrated deduction system provides proof support for the deduction problems arising during the development process. We describe the application of VSE to an industrial case study and give an overview of the enhanced VSE system and the VSE methodology.     

Software development tools for microcontrollers

Two software tools are described that are designed to facilitate software development for microcontrollers. One is a mid-level programming language called Pascal/48 and the other is a circuit simulation system. Pascal/48 is designed to give the programmer many of the advantages of a high-level language, but also provide access to all of the hardware of the Intel MCS-48 series of microcontrollers. The circuit simulation system combines many of the advantages of simulation and emulation. It provides a software testing environment in which many more software functions can be tested than with conventional simulators. The system integrates an instruction-set simulator with simulators for other devices. They operate in parallel and are synchronized by a clock that records simulated time. I/O lines of the microcontroller can be linked to other components so that complete circuits can be simulated. Displays are provided of the internal and external state of the simulated circuit, and of the Pascal/48 program being executed. They are updated as simulated execution proceeds using the screen updating facilities of ASCII terminals. Simulation can be continuous, single step, or execution can be reversed (i.e. instructions are ‘unexecuted’).     

Experiences with incorporating formal techniques into industrial practice

We report about experiences at Philips Healthcare with component-based development supported by formal techniques. The formal Analytical Software Design (ASD) approach of the company Verum has been incorporated into the industrial workflow. The commercial tool ASD:Suite supports both compositional verification and code generation for control components. For other components test-driven development has been used. We discuss the results of these combined techniques in a project which developed the power control service of an interventional X-ray system.     

Software tools for safety-critical software development

We briefly present a software methodology for safety-critical software, developed over many years to cope with industrial safety-critical applications in the Canadian nuclear industry. Following this we present discussion on software tools that have been used to support this methodology, and software tools that could be used, but have not been used for a variety of reasons. Based on our experience, we also present and motivate a list of high-level requirements for tools that would facilitate the development of safety-critical software using the presented methods, together with a small number of tools that we believe are worth developing in the future.     

A formal methodology using attributed grammars for multiprocessing-system software development. I. Design representation

With the growing complexity of multiprocessing systems and distributed computing systems, there is an increasing need to provide a formal methodology for deriving a model to represent software design for the software development of these systems. The formal methodology presented in this paper uses attributed grammars, and extends formal methods commonly used in the definition of programming languages and compiler techniques for representing the design specification of software systems and validating the implementation. This model provides a common basis in the software development phases through automated design analysis, test-case generation, and validation of the software system. This paper covers the construction of the model for the design representation using attributed grammar and the analysis of the software system design based on the model.     

Ready for testing: ensuring conformance to industrial standards through formal verification

The design of distributed, safety-critical real-time systems is challenging due to their high complexity, the potentially large number of components, and complicated requirements and environment assumptions that stem from international standards. We present a case study that shows that despite those challenges, the automated formal verification of such systems is not only possible, but practicable even in the context of small to medium-sized enterprises. We considered a wireless fire alarm system, regulated by the EN 54 standard. We performed formal requirements engineering, modeling and verification and uncovered severe design flaws that would have prevented its certification. For an improved design, we provided dependable verification results which in particular ensure that certification tests for a relevant regulation standard will be passed. In general we observe that if system tests are specified by generalized test procedures, then verifying that a system will pass any test following those test procedures is a cost-efficient approach to improve the product quality based on formal methods. Based on our experience, we propose an approach useful to integrate the application of formal methods to product development in SME.     

DHP算法优化控制开发工具的设计与实现

针对目前自适应动态规划的研究中大多采用Matlab语言编程,存在代码执行效率低、使用不灵活等缺点,采用面向对象的编程技术和C++语言设计了一种基于双启发式动态规划算法(DHP)和执行依赖双启发式动态规划(ADDHP)算法的优化控制开发工具,介绍了开发工具的设计开发思路、工作流程、功能特点、主要界面和使用方法.将该工具用于三容液位实验装置的实时仿真控制,实验结果表明,该开发工具具有使用灵活、训练速度快、执行效率高等优点.     

A formal approach for the development of reactive systems

Context

This paper deals with the development and verification of liveness properties on reactive systems using the Event-B method. By considering the limitation of the Event-B method to invariance properties, we propose to apply the language TLA⁺ to verify liveness properties on Event-B models.

Objective

This paper deals with the use of two verification approaches: theorem proving and model-checking, in the construction and verification of safe reactive systems. The theorem prover concerned is part of the Click_n_Prove tool associated to the Event-B method and the model checker is TLC for TLA⁺ models.

Method

To verify liveness properties on Event-B systems, we extend first the expressivity and the semantics of a B model (called temporal B model) to deal with the specification of fairness and eventuality properties. Second, we propose semantics of the extension over traces, in the same spirit as TLA⁺ does. Third, we give verification rules in the axiomatic way of the Event-B method. Finally, we give transformation rules from a temporal B model into a TLA⁺ module. We present in particular, our prototype system called B2TLA⁺, that we have developed to support this transformation; then we can verify liveness properties thanks to the model checker TLC on finite state systems. For the verification of infinite-state systems, we propose the use of the predicate diagrams and its associated tool DIXIT. As the B refinement preserves invariance properties through refinement steps, we propose some rules to get the preservation of liveness properties by the B refinement.

Results

The proposed approach is applied for the development of some reactive systems examples and our prototype system B2TLA⁺ is successfully used to transform a temporal B model into a TLA⁺ module.

Conclusion

The paper successfully defines an approach for the specification and verification of safety and liveness properties for the development of reactive systems using the Event-B method, the language TLA⁺ and the predicate diagrams with their associated tools. The approach is illustrated on a case study of a parcel sorting system.     

Knowledge-based tools for development of engineering theories

An approach to solving of the knowledge integration problem on the basis of engineering theories had been considered by Vittikh (Artif. Intell. Engng, 1997, 11). Current paper describes constraint-oriented tools for generation of engineering models which are organized around a constraint-oriented knowledge base. It also allows use of them for maintaining this approach. Many efforts in the field of artificial intelligence are concentrated on solving geometric constraint satisfaction problems in a specific domain. This paper describes the solving of a geometric constraint system called ANMEC that has been created with the use of these tools. The way the system is applied to tasks of mechanism's analysis and synthesis is considered.