Smooth adoption of Verum’s Dezyne to model software for a service tool
First experiences with Dezyne
Saurav Paul was introduced to the methodology of Model Driven Engineering during his Master study Embedded Systems at the Technical University of Delft. When attending a Dezyne Community meeting shortly after his graduation, he recognized a strong parallel between the tool and what he had learned at university. Enthusiastic about the possibilities, he started using the toolset for a small software design project. “According to me Model Driven Engineering is the future of software development,” Saurav says. “So I was eager to start using Dezyne.”
Combining high-level and low-level control logic
After his graduation Saurav Paul started working for ICT Group. He was chosen as the software engineer in a project commissioned by Philips. In this project Dezyne was used as the primary toolset. Philipsdevelops x-ray systems for image guided medical procedures. The x-ray machines are powered by complex startup/shutdown controllers that ensure reliability and safety. As the behavior of these controllers is complex, a dedicated service tool is used to check and service them. Saurav designed the software for this new service tool.
Dezyne’s approach is to start by creating a model that captures the behavior of the software system. The model serves as a means of communication between software designer(s) and stakeholders. It ensures that the requirements formulated by the stakeholders are thorough, complete and effectively implemented. Dezyne also allows the software engineer to simulate software behavior at every step of the development process, which helps to verify whether the system meets the requirements. Once tested and verified, computer code is automatically generated from the model with the press of a button.
Dezyne’s unique feature: formal verification
What distinguishes the tool from other Model Driven Engineering toolsets is its built-in formal verification engine. With one click the model is scanned for errors and checks for unwanted properties like deadlocks, livelocks, incomplete mapping of events and responses, race conditions, illegal actions and compliance. When something is wrong, the verification engine not only finds the error but also pinpoints its exact location within the model.
The formal verification functionality greatly helped Saurav Paul in designing the software for the service tool. “When you commit an error while programming in the traditional way, it may be detected by the compiler. But runtime errors are very difficult to detect and debug. Yet the software shows you immediately where the mistake is located. After solving the error you can test and verify very quickly from the model. In traditional programming this takes much longer.
Ensuring correct functionality by combining TDD and Model Driven Engineering
The service tool Saurav Paul worked on has four functionalities or features: ‘manual mode’, ‘diagnose’, ‘firmware install’ and ‘save data’. In order to ensure whether these functionalities were working properly, Saurav used a combination of Test Driven Development (TDD) and Model Driven Engineering.
In traditional software development testing takes up a lot of time. Due to time pressure thorough testing is therefore often not feasible. This increases the likelihood of errors showing up later when the software is implemented. Yet ideally, thorough testing is necessary to ensure that the software fulfils the requirements of the system. In Dezyne testing does not suffer from the same problems as it does in traditional software development.
What sets the software apart is that the testing phase is much shorter and more efficient. The components comprising a software system do not have to be tested very thoroughly, since the built-in formal verification engine already checks for unwanted properties, such as deadlocks and race conditions. The only thing left to be tested is the functionality of the entire software system. In the future Verum plans to add more functional property checking, so that eventually functional correctness can be formally verified and does not need to be tested separately.
Saurav designed the software for the four functionalities of the service tool by modeling them in Dezyne. He then ran unit tests in order to verify the intended behaviour. When errors showed up during the tests, he was able to correct them quickly in the model itself before re-testing the whole system.
This combination of testing and (re)modelling results in quick and efficient adaptations, even late into the design process. Saurav Paul: “The major difference in Dezyne is that you spend more time on design and less time on testing. Because of its formally verified implementation, Dezyne ensures quality and provides more opportunities to find and fix design issues in the initial phase of development.”
Programming by hand
Dezyne is not suited to design software for algorithms or to model data flow. These features have to be programmed by hand. Saurav Paul: “Whenever the software had to take data based decisions or read data, we used handwritten code instead of the model.” Handwritten code was also used to glue the software to the pre-existing code of the outside environment, the Startup/Shutdown controller. Saurav then ran final integration tests to see whether the new software was working properly with the startup/shutdown controller. This ensured the successful completion of the project.