Journal papers
- T.S. Hoang
, C. Snook
, A. Salehi
,
M. Butler
, and L. Ladenberger
. Validating and verifying the requirements and design of a haemodialysis machine using the Rodin toolset. In
Science of Computer Programming, November 2017
© Elsevier (abstract, bibtex, pdf, link).
- A. Fürst
, T.S. Hoang
, D. Basin
,
N. Sato
, and K. Miyazaki
. Large-scale system
development using Abstract Data Types and refinement. In
Science of Computer Programming, 131:59-75, December 2016
© Elsevier (abstract, bibtex, pdf, link).
- T.S. Hoang
, S. Schneider
, H. Treharne
, and D. Williams
. Foundations for using linear
temporal logic in Event-B refinement. In Formal Aspects of
Computing, 28(6):909-935, March 2016 © Springer-Verlag
(abstract, bibtex, link).
- S. Hudon
, T.S. Hoang
, and J. Ostroff
. The Unit-B method: refinement guided by progress
concerns.. In Software and System Modeling,
15(4):1091-1116, February 2016 © Springer-Verlag (abstract, bibtex, pdf, link).
- S. Hallerstede
, T.S. Hoang
. Refinement of
Decomposed Models by Interface Instantiation. In Science of
Computer Programming, 94(2):144-163, November 2014 ©
Elsevier (abstract, bibtex, pdf, link).
- T.S. Hoang
. Reasoning about Almost-Certain
Convergence Properties Using Event-B. In Science of
Computer Programming, 81:108-121, February 2014 ©
Elsevier (abstract, bibtex, pdf,
link).
- T.S. Hoang
, A. McIver
, L. Meinicke
,
C. Morgan
, A. Sloane
, E. Susatyo
. Abstractions of Non-interference Security: Probabilistic
versus Possibilistic. In Formal Aspects of Computing,
26(1):169-194, January 2014 © Springer-Verlag (abstract, bibtex, link).
- N. Sato
, T.S. Hoang
, D. Basin
, and
H. Kuruma
. Verification for Monitoring Requirements of
Train Monitoring Systems in Event-B. In Information
Processing Society of Japan Journal, 54(6):1738-1750, July
2013 © Information Processing Society of Japan (abstract,
bibtex,
pdf, link).
- T.S. Hoang
, A. Fürst
and J-R. Abrial
. Event-B Patterns and Their Tool Support. In Software
and Systems Modelling, 12(2):229-244, 2013 ©
Springer-Verlag (abstract, bibtex, pdf,
link).
- T.S. Hoang
. Security Invariants in Discrete
Transition Systems. In Formal Aspects of Computing
25(1):59-87, 2013 © Springer-Verlag (abstract, bibtex, pdf, link).
- R. Silva
, C. Pascal
, T.S. Hoang
and
M. Butler
. Decomposition Tool for Event-B. In
Software: Practice & Experience, January 2011 © John
Wiley & Sons, Ltd (abstract, bibtex, pdf,
link).
- J-R. Abrial
, M. Butler
, S. Hallerstede
, T.S. Hoang
, F. Mehta
and L. Voisin
. Rodin: an Open Toolset for Modelling and Reasoning in
Event-B. In International Journal on Software Tools for
Technology Transfer (STTT), April 2010 © Springer-Verlag
(abstract, bibtex, pdf, link).
- T.S. Hoang
, H. Kuruma
, D. Basin
and
J-R. Abrial
. Developing Topology Discovery in
Event-B. In Science of Computer Programming, Volume 74,
Issues 11-12, November 2009, pages 879-899 © Elsevier (abstract, bibtex, pdf, link).
- S. Schneider
, T.S. Hoang
, K. Robinson
and H. Treharne
. Tank Monitoring: a pAMN Case
Study. Formal Aspects in Computing, volume 18, number
3, September 2006 © Springer-Verlag. (abstract, bibtex, @ S. Schneider's website, link).
Conference papers
- M. Butler
, D. Dghaym
, T. Fischer
,
T.S. Hoang
, K. Reichl
, C. Snook
, and
P. Tummeltshammer
. Formal Modelling Techniques for
Efficient Development of Railway Control Products. In
RSSRail2017: Proceedings of the Second International Conference
on Reliability, Safety, and Security of Railway
Systems. Modelling, Analysis, Verification, and Certification,
volume 10598 of Lecture Notes in Computer Science, pages
71–86, Pistoia, Italy, November 2017 © Springer (abstract,
bibtex,
Soton ePrint).
- T.S. Hoang
, D. Dghaym
, C. Snook
, and
M. Butler
. A Composition Mechanism for
Refinement-Based Methods. In The 22nd International
Conference on Engineering of Complex Computer Systems (ICECCS
2017), Fukuoka, Japan, November 2017 © IEEE (Soton
ePrint).
- C. Bogdiukiewicz
, M. Butler
, T.S. Hoang
, M. Paxton
, J. Snook
, X. Waldron
,
and T. Wilkinson
. Formal Development of Policing
Functions for Intelligent Systems. In The 28th
International Symposium on Software Reliability Engineering
(ISSRE) - IEEE, Toulouse, France, October 2017 © IEEE (Soton
ePrint).
- T.S. Hoang
, C. Snook
, D. Dghaym
, and
M. Butler
. Class-diagrams for Abstract Data
Types. In ICTAC2017, volume 10580 of Lecture Notes
in Computer Science, pages 100–117, Hanoi, Vietnam, October 2017
© Springer (abstract,
bibtex,
Soton ePrint).
- C. Snook
, T.S. Hoang
, and M. Butler
. Analysing Security Protocols Using Refinement in
iUML-B. In NASA Formal Methods - 9th International
Symposium, NFM 2017, pages 84–98, Moffett Field, CA, USA, May
2017 © Springer (abstract, bibtex, pdf, Soton
ePrint).
- T.S. Hoang
, C. Snook
, L. Ladenberger
, M. Butler
. Validating the Requirements and Design
of a Hemodialysis Machine Using iUML-B, BMotion Studio, and
Co-Simulation. In ABZ2016, volume 9675 of Lecture
Notes in Computer Science, pages 360–375, Linz, Austria, May
2016 © Springer-Verlag (abstract, bibtex, pdf, link).
- T.S. Hoang
, Shinji Itoh
, Kyohei Oyama
, K. Miyazaki
, H. Kuruma
, N. Sato
. Consistency Verification of Specification Rules. In
ICFEM 2015, volume 9407 of Lecture Notes in Computer
Science, pages 50–66, Paris, France, November 2015 ©
Springer-Verlag (abstract, bibtex, pdf, link).
- A. Fürst
, T.S. Hoang
, D. Basin
,
K. Desai
, N. Sato
, and K. Miyazaki
. Code Generation for Event-B. In IFM, volume 8737
of Lecture Notes in Computer Science, pages 323–338,
Bertinoro, Italy, September 2014 © Springer-Verlag (abstract, bibtex, pdf,
link).
- G. Ciobanu
, T.S. Hoang
, A. Stefanescu
. From TiMo to Event-B: Event-Driven Timed Mobility. In
Proceedings of the 19th IEEE International Conference on
Engineering of Complex Systems (ICECCS 2014), pages 1-10,
Tianjin, China, August 2014 (abstract,
bibtex,
pdf, link)). Awarded Best
Paper.
- A. Fürst
, T.S. Hoang
, D. Basin
,
N. Sato
, and K. Miyazaki
. Formal System
Modelling Using Abstract Data Types in Event-B. In ABZ,
volume 8477 of Lecture Notes in Computer Science, pages
222–237, Toulouse, France, June 2014 © Springer-Verlag (abstract, bibtex, pdf, link).
- S. Hudon
and T.S. Hoang
. Systems Design
Guided by Progress Concerns. In Integrated Formal
Methods, volume 7940 of Lecture Notes in Computer
Science pages 16-30, Turku, Finland, June 2013 ©
Springer-Verlag (abstract, bibtex, pdf, link, slides, 4-up handout).
- S. Hallerstede
and T.S. Hoang
. Refinement
by Interface Instantiation. In , volume 7316 of Lecture Notes in
Computer Science, pages 223-237, Pisa, Italy, June 2012 ©
Springer-Verlag (abstract, bibtex, pdf,
link).
- T.S. Hoang
and J-R. Abrial
. Reasoning about
Liveness Properties in Event-B. In Formal Methods and
Software Engineering, volume 6991 of Lecture Notes in
Computer Science, pages 456-471, Durham, United Kingdom,
October 2011 © Springer-Verlag (abstract, bibtex, pdf, link, slides, print (slides)).
- T.S. Hoang
and J-R. Abrial
. Event-B
Decomposition for Parallel Programs. In Abstract State
Machine, Alloy, Event-B and Z, volume 5977 of Lecture
Notes in Computer Science, pages 319-333, Orford, Canada,
February 2010 © Springer-Verlag (abstract, bibtex, pdf, link, slides, print (slides)).
- T.S. Hoang
, A. Fürst
and J-R. Abrial
. Event-B Patterns and Their Tool Support. In Software
Engineering and Formal Methods, pages 210-219, Hanoi, Vietnam,
November 2009 © IEEE Computer Society (abstract, bibtex, pdf,
link, slides, print (slides)).
- T.S. Hoang
, H. Kuruma
, D. Basin
and
J-R. Abrial
. Developing Topology Discovery in
Event-B. In Integrated Formal Methods, volume 5423 of Lecture Notes in Computer
Science, pages 1-19, Düsseldorf, Germany, February 2009
© Springer-Verlag (abstract, bibtex, pdf, link).
- J-R. Abrial
, T.S. Hoang
. Using Design
Patterns in Formal Methods: An Event-B Approach. In
International Colloquium on Theoretical Aspects of
Computing, volume 5160 of Lecture Notes in Computer
Science, pages 1-2, Istanbul, Turkey, September 2008 ©
Springer-Verlag (bibtex, link).
- S. Hallerstede
, T.S. Hoang
. Qualitative
Probabilistic Modelling in Event-B. In Integrated Formal
Methods, volume 4591 of Lecture Notes in Computer
Science, pages 293-312, Oxford, UK, July 2007, ©
Springer-Verlag (abstract, bibtex, pdf, link). Awarded Best
Paper.
- C. Morgan
, T.S. Hoang
and J-R. Abrial
. The Challenge of Probabilistic
Event-B. ZB2005: Formal Specification in Z and
B, volume 3455 of Lecture Notes in Computer
Science, pages 162-171, Guildford, UK, April 2005 ©
Springer-Verlag (abstract, bibtex, link).
- T.S. Hoang
, Z. Jin
, K. Robinson
,
A. McIver
, and C. Morgan
. Development via
Refinement in Probabilistic B --- Foundation and Case
Study. ZB2005: Formal Specification in Z and B, volume
3455 of Lecture Notes in Computer Science, pages
355-373, Guildford, UK, April 2005 © Springer-Verlag (abstract,
bibtex,
pdf, link, slides, print (slides)).
- A. McIver
, C. Morgan
, and T.S. Hoang
. Probabilistic Termination in B. In D. Bert, J.P. Bowen,
S. King, and M. Waldén, editors, ZB2003: Formal
Specification and Development in Z and B, volume 2651 of Lecture Notes in Computer
Science, pages 216-239, Turku, Finland, June 2003 ©
Springer-Verlag (abstract, bibtex, @ C. Morgan's website, link). Awarded Best
Paper.
- T.S. Hoang
, Z. Jin
, K. Robinson
,
A. McIver
, and C. Morgan
. Probabilistic
Invariant for Probabilistic Machines. In D. Bert, J.P. Bowen,
S. King, and M. Waldén, editors, ZB2003: Formal
Specification and Development in Z and B, volume 2651 of Lecture Notes in Computer
Science, pages 240-259, Turku, Finland, June 2003 ©
Springer-Verlag (abstract, bibtex, pdf, link, slides, 4-page poster).
Book chapters
- D. Basin
and T.S. Hoang
. Technology
transfer. In A. Romanovsky and M. Thomas, editors,
Industrial Deployment of System Engineering Methods,
chapter 13, pages 187-196, July 2013 © Springer-Verlag (abstract, bibtex, pdf, link)
- T.S. Hoang
. An Introduction to the Event-B
Modelling Method. In A. Romanovsky and M. Thomas, editors,
Industrial Deployment of System Engineering Methods, pages
211-236, July 2013 © Springer-Verlag (abstract, bibtex, pdf, link)
Workshop papers
- T.S. Hoang
, N. Sato
, Tomoyuki Myojin
,
M. Butler
, Yuichiroh Nakagawa
, and Hideto Ogawa
. Policing Functions for Machine Learning
Systems. In
Workshop on Verification and Validation of Autonomous Systems (abstract,
bibtex,
link).
- T.S. Hoang
. Proof hints for Event-B. In
Proceedings of the DS-Event-B-2012 Workshop (abstract,
bibtex,
link).
- D. Basin
, A. Fürst
, T.S. Hoang
,
K. Miyazaki
, and N. Sato
. Abstract data types
in Event-B - An application of generic instantiation. In
Proceedings of the DS-Event-B-2012 Workshop (abstract, bibtex, link).
- T.S. Hoang
, A. Illiasov, R. Silva
,
W. Wei. A Survey on Event-B Decomposition. In
Proceedings of the 11th Automatic Verification of Critical
Systems (AVoCS 2011), volume 46 of Electronic
Communications of the EASST (abstract, bibtex, link).
- T.S. Hoang
, A. McIver
, L. Meinicke
,
A. Sloane
, E. Susatyo
. Automated Analysis of
Non-interference Security by Refinement. In Proceedings
of the CryptoForma Workshop 2011, Limerick, Ireland, June,
2011 (abstract,
BiBTeX,
slides, 4-up handout).
- S. Hudon
, T.S. Hoang
. Development of
Control Systems Guided by Models of their Environment. In
Proceedings of the B 2011 Workshop, volume 280 of
Electronic Notes in Theoretical Computer Science, December 2011,
pages 57-68 © Elsevier (abstract, bibtex, link, slides, 4-up
handout).
- E. Yilmaz
and T.S. Hoang
. Development of
Rabin's Choice Coordination Algorithm in Event-B. In
Proceedings of the 10th Automatic Verification of Critical
Systems (AVoCS 2010), volume 35 of Electronic
Communications of the EASST (abstract, bibtex, link, slides (use Acrobat Reader for animation), 4-up
handout).
- R. Silva
, C. Pascal
, T.S. Hoang
and
M. Butler
. Decomposition Tool for Event-B. In
Workshop on Tool Building in Formal Methods - ABZ2010
Conference, 22nd February 2010, Orford, Quebec, Canada (abstract,
bibtex,
link @ University of Southampton).
- S. Schneider
, T.S. Hoang
, K. Robinson
and H. Treharne
. Tank Monitoring: a pAMN Case
Study. Electronic Notes in Theoretical Computer Science
(ENTCS), volume 137, number 2, April 2005, © Elsevier.
(abstract, bibtex, pdf, link).