Computer-checked models can be used to prove that core communications and state management in a software program are 100% logically correct. Such models can also be used to generate 100% correct source code. The usage of formal methods can reduce costs and time to market and help to deliver highly reliable software products.
What do ACTA, SEPA, PIPA, Stuxnet, Google have in common? They all have been hot topics in the press during the last months and they are dealing with information security. What, however, is commonly forgotten are internal threats related to espionage and stealing of company information.
In a recent news report CNN has revealed a translated Toyota memo which links problems of the car manufacturer regarding an electronic acceleration concern to a software issue. When even news magazines pick up such stories, this shows the growing importance of software for embedded systems.