COM1001 attendance monitoring

Automated abstraction of code into a state-based specification and test generation

In traditional software development, specification and testing do not play an important role. In particular, changes to software code do not normally get reflected in a specificaton. At the same time, specification-based testing methods are very important for maintaing software quality, for identification of missing or incorrectly-implemented behaviour. The project aims to develop a method and a tool to take an incomplete state-based specification, hints for developers as to how it relates to code and both extract a complete (up-to-date) specification and generate tests from it.

A number of existing specificaton-based testing methods rely on a program under test being built with testing in mind, and loose a lot in power if this is not true. In this project, observation of program behaviour under test will be used to make up for the missing information about a system, making it more amenable to testing using these methods.

More details on the completed project are at here. A follow-on project called REGI started in April 2009 and finished in 2012.

Present occupation

Lecturer from 1 Sep 2000, working at the Department of Computer Science, The University of Sheffield, UK.

Previously a research associate (RA) from 1 Oct 99 until 31 Aug 2000 in the Department of Computer Science, The University of Sheffield, UK on the EPSRC-funded MOTIVE project. The research focused on testing of object-oriented systems using an X-machine testing method.

I am a member of the Verification and Testing Research Group.


I have finished the Ph.D degree in Computer Science, in the area of specification-based software testing, in April 2000. The thesis is available. My research focused to bring the achievements of the X-machine testing method, for testing software against its specifications in Statecharts. My supervisor was Prof. Mike Holcombe and I was funded by the Daimler-Chrysler AG, Berlin.

X-machines are the extension of finite-state machines, with memory. When transitions are taken, some functions are executed which take input and produce output, using and possibly modifying this memory. This extension allows to build powerful systems without the state explosion of finite-state machines. The real benefit is in testing: it is possible to lay down reasonable assumptions for the specification and development process and construct a test set. If this test set does not reveal faults, the whole implementation could be considered behaviourally-equivalent to the specification. To put this statement in other words, unlike many testing methods, the X-machine one puts down all assumptions which are made.

Statecharts is the widely-known formalism for specification of systems. Like X-machines, it is also an extension of finite-state machines, but it contains many more elements, such as state hierarchy and concurrency.

My Ph.D. research concentrated at an application of the X-machine testing method to testing of implementations against specifications for software specified in Statecharts. The aim was to preserve the provable correctness provided by the X-machine testing method by adapting it to a subset of statecharts which excludes only a few elements.

Some of the recent publications


M. Soucha, K. Bogdanov State identification sequences from the splitting tree. Information and Software Technology, Vol. 123, Jul 2020.


M. Soucha, K. Bogdanov Observation tree approach : active learning relying on testing. The Computer Journal, 2019.


M. Soucha, K. Bogdanov SPYH-Method: An Improvement in Testing of Finite-State Machines. In proceedings of Advances in Model-based Testing (A-MOST), 2018: 194-203


T. Arts, K. Bogdanov, A. Gerdes, J. Hughes. "Graphical editing support for QuickCheck models" In Proceedings of TAIC PART, a workshop of ICST, 2015.


P. Seijas, S. Thompson, R. Taylor, K. Bogdanov, J. Derrick "Synapse: automatic behaviour inference and implementation comparison for Erlang". Erlang Workshop 2014: 73-74


R. Taylor, K. Bogdanov, J. Derrick. "Automatic Inference of Erlang Module Behaviour" In Proceedings of the International Conference on Integrated Formal Methods (iFM) 2013.


N. Walkinshaw, K. Bogdanov "Automated Comparison of State-Based Software Models in terms of their Language and Structure" ACM Transactions on Software Engineering and Methodology, Volume 22, Issue 2.


N. Walkinshaw, B. Lambeau, C. Damas, K. Bogdanov, P. Dupont1. "STAMINA: A Competition to Encourage the Development and Assessment of Software Model Inference Techniques", Journal of Empirical Software Engineering.


Ramsay Taylor and Mathew Hall and Kirill Bogdanov and John Derrick "Using behaviour inference to optimise regression test sets", 24th IFIP Int. Conference on Testing Software and Systems (ICTSS).


Neil Walkinshaw and Kirill Bogdanov, "Adapting Grammar Inference Techniques to Mine State Machines", in book Mining Software Specifications: Methodologies and Applications Editor(s): David Lo; Siau-Cheng Khoo; Jiawei Han; Chao Liu. Published by CRC press.


Kirill Bogdanov, "Test generation for X-machines with non-terminal states and priorities of operations", in proceedings of the Fourth IEEE International Conference on Software Testing, Verification and Validation. (ICST 2011), Berlin.


Neil Walkinshaw, Kirill Bogdanov, John Derrick and Javier Paris. "Increasing Functional Coverage by Inductive Testing: A Case Study", in proceedings of ICTSS 2010, Natal, Brazil.


N. Walkinshaw, K. Bogdanov, C. Damas, B. Lambeau, P. Dupont, "A Framework for the Competitive Evaluation of Model Inference Techniques", in proceedings of the 1st International Workshop on Model Inference In Testing (MIIT10), Trento, Italy.


Kirill Bogdanov, Neil Walkinshaw, "Computing the Structural Difference between State-Based Models". In Proceedings of the Working Conference on Reverse Engineering (WCRE) 2009, pp. 177-186


Robert M. Hierons, Kirill Bogdanov, Jonathan P. Bowen, Rance Cleaveland, John Derrick, Jeremy Dick, Marian Gheorghe, Mark Harman, Kalpesh Kapoor, Paul Krause, Gerald Lü, Anthony J. H. Simons, Sergiy A. Vilkomir, Martin R. Woodward, Hussein Zedan. "Using formal specifications to support testing". ACM Computing Surveys, 41(2)


Chapter "Testing from X-Machine Specifications" in the collection of papers "Formal Methods and Testing", R. Hierons, J. Bowen and M. Harman (editors). Series: Lecture Notes in Computer Science, Vol. 4949. ISBN: 978-3-540-78916-1. Link to the publisher's site and link to the chapter.


Most publications for two years are available on the Neil Walkinshaw's page.


K.Bogdanov and M.Holcombe and F.Ipate and L.Seed and S. Vanak (alphabetical order). "Testing methods for X-machines, a review". to appear in Formal Methods of Computer Science in 2006.


Bogdanov K, Holcombe M. "Testing from object machines in practice". In: Proceedings of UK Software testing research III workshop (UKTest), 2005.


K. Bogdanov and M.Holcombe. "Refinement in statechart testing". Software Testing, Verification and reliability, 14(3), September 2004. This is a revised version of the paper which appeared in Softest-II.


K. Bogdanov and M.Holcombe. "Refinement in statechart testing", in the proceedings of the workshop Softest-II, University of York, UK.


A J H Simons, M P Stannett, K E Bogdanov and W M L Holcombe. "Plug and Play Safely: Rules for Behavioural Compatibility", Proc. 6th IASTED Int. Conf. Software Engineering and Applications, (Cambridge MA: IASTED, 2002), 263-268.


K. Bogdanov. "Three Challenges in Blackbox Testing", in the position statement of the panel session `FORTEST: Formal Methods and Testing' held at COMPSAC'2002, Oxford. Proceedings published by IEEE Computer Society.


K.Bogdanov, M.Holcombe. "Testing from statecharts using the Wp method", in the proceedings of the CONCUR'02 Satellite Workshop on Formal Approaches To Testing (FATES), 2002.


K.Bogdanov, M.Holcombe. "Properties of concurrently taken transitions of Harel statecharts", in the proceedings of the ETAPS Satellite Workshop on Semantic Foundations of Engineering Design Languages (SFEDL), 2002.


M. Holcombe, K. Bogdanov, and M. Gheorghe. "Functional test generation for Extreme Programming", Second International Conference on eXtreme Programming and Flexible Processes in Software Engineering (XP2001), 2001.


K.Bogdanov, M.Holcombe. "Testing of software using X-machines", in collection"Methods and Aids of Developing Document Flow Systems", Russian Academy of Sciences, Institute of System Analysis, Editors: Prof. V.L. Arlazarov, Prof. N.E. Emelyanov, Russia (in Russian)


K. Bogdanov and M. Holcombe. " Statechart testing method for aircraft control systems", Software testing, verification and reliability, 11:39--54, 2001.


K.Bogdanov, M.Holcombe, H.Singh "Automated Test Set Generation for Statecharts", in D. Hutter, W. Stephan, P. Traverso and M. Ullmann, editors, Applied Formal Methods - FM-Trends 98, volume 1641 of Lecture Notes in Computer Science, pages 107-121, Springer Verlag, 1999.


K.Bogdanov, O.Slavin "Merging of sequences of recognition results", in collection"Intellectual Technologies of Information Input and Processing", Russian Academy of Sciences, Institute of System Analysis, Russia (in Russian)


K.Bogdanov, M.Fairtlough, M.Holcombe, F.Ipate, C.Jordan "X-machine Specification and Refinement of Digital Devices", Technical Report
CS-97-16,University of Sheffield, Department of Computer Science.


K.Bogdanov "Merging sequences of objects", in proceedings of the international workshop "Dialogue'95: Computational Linguistics and its Applications", Kazan, Russia

Presentations at conferences and workshops


K.Bogdanov, M.Holcombe, H.Singh "Test Generation From Statemate Specifications", Testing Workshop, Sep 17-18 1998, York, UK. Sheffield, Department of Computer Science.


K.Bogdanov, M.Holcombe, H.Singh "Testing Statemate Models", presented at the "X-Machines Day", Jul 24 1998, Department of Computer Science, University of Sheffield, UK.


M.Holcombe, K.Bogdanov "The third step towards correct software", BCTCS 13: British Colloquium for Theoretical Computer Science, Mar 26-27 1997, Sheffield, UK.


K.Bogdanov, M.Holcombe "The mapping between mSZ statecharts and X-machines", ESPRESS Workshop, Jan 24-25, 97, Berlin, Germany.

Related research interests


Join the Blue Ribbon Online Free Speech Campaign!
Protect privacy online : join the Golden Key Campaign!

Comments ? feel free to email me (replace _ in the email address with @)

My address is:

Department of Computer Science
The University of Sheffield
Regent Court
211 Portobello St.
Sheffield S1 4DP
Tel:+44 (0) 114 2221847