Reliable Software with Complex Behavior Development

Andrew Borisenko, Pavel Fedotov, Oleg Stepanov, Anatoly Shalyto

An important part of creating systems with complex behavior is quality control. Regression makes it important not just to check that the developed program satisfies all its requirements, but also make this process efficient, maximally automate it. In practice, this can be done with formalized program requirements and keeping of executable specification together with the code of the program.

This paper focuses on improvement of presentation of specifications for automata programs where complex behavior is expressed in a number of explicitly separated states. We show how to formalize specifications using tests, temporal formulas and contracts and integrate these presentations into integrated development process. We also suggest how to preserve the correctness of automata programs during redesign of complex behavior.

Anatoly Shalyto

Bio

Anatoly Abramovich Shalyto is a Russian scientist, doctor of sciences, professor, awarded by Russian State Government in 2008 for achievements in education, developer of technology for Automata-based programming named “Switch-technology”, initiator of Open Project Documentation Initiative and of “Save the best in the universities of Russia”.

Anatoly Shalyto introduced a Switch-technology — technology for Automata-Based Programming.
He is also a coauthor of a UniMod tool that supports Automata-Based Programming, initiator of Foundation for Open Project Documentation.

Author of a series of articles devoted to the problems of Computer Science and education in Russia.

Anatoly Shalyto also has scientific results in Boolean functions and Logic Control.

Andrey Borisenko

Bio

Andrey graduated from Saint-Petersburg Physic-Mathematical lyceum #239.

Now he is a student of Saint-Petersburg State University of Information Technologies, Mechanics and Optics.

Holds a Bachelor’s degree for research of finite-state machine verification.

Oleg Stepanov

Bio

Oleg graduated from Saint-Petersburg Physic-Mathematical School №30.
Holds a Master’s degree from the Saint-Petersburg State University of Information Technologies, Mechanics and Optics.

Now he combines a postgraduate education with department management in JetBrains.

The sphere of his scientific interests includes dynamic and object-oriented languages, multilingual environments, Automata-based programming and development environments.

Pavel Fedotov

Bio

Pavel graduated from Saint-Petersburg Physic-Mathematical lyceum #239.
Now he is a student of Saint-Petersburg State University of Information Technologies, Mechanics and Optics.
Holds a Bachelor’s degree for research of finite-state machines refactoring.