In 2018 and 2019, the Boeing 737 Max experienced two tragic crashes that resulted in 346 casualties, leading the aircraft to be grounded across 40 countries, including Korea. The Maneuvering Characteristics Augmentation System (MCAS), software designed to prevent nosedives, was to blame. This serves to demonstrates that the rapidly increasing application of software could create numerous software-induced accidents that result in equally catastrophic damage.

The Software Verification Laboratory (SV Lab) directed by Professor Kyungmin Bae at the Department of Computer Science and Engineering, POSTECH, is developing technologies, theories, algorithms and tools that improve software reliability and safety while preventing errors. Thus far, developers have been manually testing the software to verify that it executes the desired outcomes. However, as the complexity of software grows and its development cycle shortens, such manual testing faces limitations.

The Lab is working on a ‘cyber-physical system’ that enables the verification of software that is required to operate devoid of any margin of error on such physical objects as automobiles or airplanes. The cyber-physical system software functions in an environment that changes virtually every second. For example, a car traveling at 100km/h hits the brakes instantly upon recognizing a hazard in its periphery. Conventional software verification technology has only been capable of identifying logical errors in software; there was no way to verify complex physical requirements that change with the surroundings.

The Lab was the world’s first to present theories to formally verify varying situations that unfold within the cyber-physical system through the use of logic languages, and it developed algorithms and tools based on these theories. Essentially, this helps in constructing a software-regulated physical environment to verify the requirements in both the physical and digital systems. Researchers at the Lab are also developing algorithms that leverage inferences to promptly handle the ‘state explosion problem’ which refers to the exponential growth in the number of cases that algorithms should analyze.

It is clear that the application of tested-and-proven software for automobiles, airplanes, infrastructure systems and within the sectors of healthcare, finance and power will be instrumental in defining the software powerhouses in the coming years . The US and Europe already have a leg up on the competition with their formation of academic societies and publications of verification tools. According to Professor Bae, the ultimate aim of the Software Verification Laboratory is to “emerge as a global leader in developing verified software and to contribute to the overall safety of society’s infrastructure”.