Form offers tailor-made solutions that integrate analytic methods into development trajectories. These solutions are a combination of model-based techniques that optimize system and business processes and that automatically detect errors. Our way of working is highly suitable for high-tech enterprises that manufacture embedded systems or develop mission critical applications. Form offers product quality improvement, lowers lead time development and reduces costs for testing through the push of a single button.
Form believes that model based verification techniques can be applied on an industrial scale. Because the verification of a system inherently involves describing the essence of a system, we do not believe that all systems can be verified using a single tool. Any such tool would have to be able to capture the meaning of any domain, thus confusing the engineer with too many parameters, or depriving him of the possibility to describe his system at an appropriate level of abstraction.
Verification significantly improves the quality of software and increases the speed of development. In our view, verification procedures for complex systems need to be tailored to the requirements of the engineers that develop those systems. Integration into a model-driven engineering approach should be possible, and the use of domain specific languages should be a primary means to achieve this.
Industry is ready to embrace formal methods as a fundamental part of their development process. Form helps to decide how and on what scale verification methods can be applied.
Many formal and model based techniques, methods and tools are currently available, and after years of development, they have finally reached a maturity level that allows them to be put to practice on an industrial scale. Form helps you select the right tools to increase your productivity and product quality, and provides solutions that can be operated and maintained by your own (domain) experts.
At Form we have a lot of experience with developing and applying formal methods in the field. We offer impact analysis as a service to show you where and how formal methods could be applied, and to what benefit. Because Form does not aim to provide one tool for every job, we unbiasedly assist in selecting the appropriate methods, techniques and tools for the job at hand.
An often heard complaint about model checkers and other formal tools is that they are hard to use. Form offers services that integrate formal tests and verification methodologies into existing system development. This minimises the increase of work load on your development trajectory, and eliminates the need to perform any adjustments to your business development process. Studies have shown life-cycle improvements of 40% and a reduction of 90% in the found number of bugs. Form offers user friendly verification, tailored to seamlessly integrate into your development process. We aspire solutions that guarantee freedom, no vendor lock-in, and no exclusive maintenance contracts. Be believe that customers should use their favourite set of tools and extend them with verification functionality.
Form facilitates model-to-model transformations that allow for models created in domain specific languages (DSLs) to be formally analysed. We define automated and processable model-to-model transformations to the appropriate analytic back-ends. This enables you to keep your favourite DSL and still optimally benefit of the latest model checking techniques.
Form offers verification to systems that already have been manufactured and show unexplainable behaviour. Concurrent reactive systems, protocols, and distributed systems operating in networks show complex behaviour that cannot be proven correct by testing alone. Our strong background in the development of complex machinery as well as formal methods enables us to capture the behaviour of a system into a model. Using this model, we analyse the system and assert that it is error free at the design level with respect to the settled system requirements.
For customers who are about to engage in a major programming effort for which the plans have already been made, we offer the possibility of design verification. Selected aspects of a software design can be modelled and proven correct. Especially for systems consisting of multiple communicating processes, this can be a real time-saver. Race conditions, deadlocks and endless loops can be detected before the product has been built.
Form helps to design distributed systems using a model-based approach. Building discrete concurrent systems is a complex and challenging task. Therefore it is crucial that such a design reflects the actual system and can be formally verified. Form assists users to design these systems in such a way that they operate efficient, while the designs can still be subjected to formal verification.
Together with LaQuSo and Vitelec, Form is involved in a special water project for South Africa. Vitelec has developed a wireless Smart Metering solution to measure the water usage per household, measure leaks in the water system, and control the water supply per household by means of a wireless controlled valve, called The Limiter. Form ensures that this system is robust and free from errors.
Flyer 2012: We believe that model based verification techniques are ready to be applied on an industrial scale. Verification significantly improves the quality of software and increases the speed of development. In our view, verification procedures for complex systems need to be tailored to the requirements of an engineer. This document describes our manifest and our solution, illustrated by several projects in which formal methods have been successfully applied.
Frank Stappers, born 24-04-1982 (Weert), obtained his Master’s degree in Computer Science (CS) at the Technische Universiteit Eindhoven (TU/e) in April 2007. Subsequently, he began to work as a Ph.D. Student at the Design and Analysis of Systems Group at the CS department of the TU/e. The first three years he was involved in the project TWINS: Optimizing Software Hardware Co-design Flow for Software Intensive Systems. In 2010 he moved to the Formal Methods Group to carry out the project LythoSysSL at ASML. In 2011 he returned to the university to write his thesis, which he defends in 2012.
Sjoerd Cranen, born 17-12-1984 (Wijchen), he graduated Cum Laude in 2008 after finishing his Master’s thesis in Sheffield, UK. From October 2008 to November 2009, he worked as a software developer for Imtech ICT Technical Systems in Amersfoort, where he was mainly working on the development of orchestration software for the Dutch and German wind tunnels in Marknesse. In November 2009, he returned to the TU/e to do a PhD study, in the HTAS Verified project. This project is a cooperation between several faculties of the TU/e , TNO and various partners in the automotive industry, in which Sjoerd participates as a member of the Model Driven Software Engineering group of the CS department.
For any inquiries or information on our products and services, please contact us at:
|t||+31(0)6 2151 0775|