Search

Many companies struggle with large amounts of legacy software that is difficult to maintain and to extend. Refactoring legacy code typically requires large efforts and introduces serious risks because often crucial business assets are hidden in legacy components. We investigate the support of formal techniques for the rejuvenation of legacy embedded software, concentrating on control components. Model learning and equivalence checking are used to improve a new implementation of a legacy control component. Model learning is applied to both the old and the new implementation. The resulting models are compared using an equivalence check of a model checker. We report about our experiences with this approach at Philips. By gradually increasing the set of input stimuli, we obtained implementations of a power control service for which the learned behaviour is equivalent.

Contains fulltext : 178513.pdf (Publisher’s version ) (Open Access)

Contains fulltext : 173201.pdf (Publisher’s version ) (Open Access)

We present a detailled timed automata model of the clock synchronization algorithm that is currently being used in a wireless sensor network (WSN) that has been developed by the Dutch company Chess. Using the UPPAAL model checker, we establish that in certain cases a static, fully synchronized network may eventually become unsynchronized if the current algorithm is used, even in a setting with infinitesimal clock drifts.

Two Domain Specific Languages (DSLs) have been developed to improve the development of a power control component of interventional X-ray systems of Philips. Configuration files and test cases are generated from instances of these DSLs. To increase the confidence in these instances and the generators, formal models have been generated to analyse DSL instances and to crosscheck the results of the generators. A DSL instance serves as a single source from which the implementation and the formal analysis models are generated. In this way, it is easy to maintain the formal support in case of changes and for new product releases. We report about our experiences with this approach in a real development project at Philips.

Contains fulltext : 155762.pdf (Publisher’s version ) (Open Access) WORLDCOMP'15 - The 2015 World Congress in Computer Science, Computer Engineering, and Applied Computing

We discuss the use of formal techniques to improve the concept phase of product realisation. As an industrial application, a new concept of interventional X-ray systems has been formalized, using model checking techniques and the simulation of formal models. cop. Springer International Publishing Switzerland 2015.

To improve the design of a power control unit at Philips, two Domain Specific Languages (DSLs) have been used. The first DSL provides a concise and readable notation for the essential state transitions. It is used to generate both configuration files and analysis models. In addition, we also generate instances of a second DSL which represents test traces. This second DSL is used to generate test cases for the power control unit. The use of DSLs not only improved productivity, but also the quality of the configuration files and the test set. cop. 2015, IEEE.

This paper describes the use of a formal method to support component-based development in the healthcare domain. The method is based on a commercial tool suite which combines formal modeling, compositional model checking, and code generation. The main approach of the tool suite will be explained and demonstrated from a user point of view. We report about experiences with this approach at the company Philips Healthcare for the design of control software for advanced interventional X-ray systems. This concerns formal interface definitions between the main system components and detailed design of control components.

Contains fulltext : 91792.pdf (Publisher’s version ) (Closed access) Foundations of Health Information Engineering and Systems - FHIES 2011: First International Symposium Johannesburg, South Africa, September 2011

In this paper we evaluate the effectiveness of applying a formal component-based approach called Analytical Software Design (ASD) to the development of control software of an industrial project at Philips Healthcare. We analyze the performance of the ASD related tasks carried out during the development processes and report about the main issues encountered. Furthermore, we investigate whether introducing these formal techniques to industry could actually improve the quality and the productivity of the developed code compared to software developed by more traditional development methods.

In this paper we apply a number of design guidelines for circumventing the state space explosion problem from [J.F. Groote, T.W.D.M. Kouters, and A.A.H. Osaiweran, Specification guidelines to avoid the state space explosion problem, 2011] to the design and formal verification of a real industrial case, namely a controller of a power distribution unit of X-ray machines developed at Philips Healthcare. Through this work we investigate whether these guidelines are effective in designing practical applications. We provide a number of alternative designs that mainly incorporate pushing and polling strategies, taking into account a number of these guidelines. Using the pushing strategy components notify one another when information becomes available while using polling components ask for information only when it is needed. We find that designs that use a pushing strategy and do not apply such guide-lines typically lead to the generation of substantially more states. All demonstrated designs formally refine a single predefined external specification that captures the desired external behavior of the system. Moreover, all designs are deadlock free and do not exhibit any illegal interactions. This confirms our hypothesis that the design guidelines are really effective in practical contexts.