Formal methods have proven helpful in modeling complex systems and ensuring they function correctly. This paper offers some basic guidelines for HFES practitioners in choosing whether to employ formal methods. It also touches on emerging approaches to modeling human behavior, attempting to answer two questions: (1) When are formal methods worth the effort? and (2) How do formal methods apply to humans? A table of questions is offered to facilitate a discussion of tradeoffs in choosing a formal methods approach.
Distribution statement A. Approved for public release: distribution unlimited.
AbbateA. J.BassE. J. (2017). Modeling affordance using formal methods. In Proceedings of the HFES annual meeting (pp. 723–727, Vol. 61). SAGE. https://doi.org/10.1177/1541931213601666
2.
AmalbertiR. (2001). The paradoxes of almost totally safe transportation systems. Safety Science, 37(2), 109–126. https://doi.org/https://doi.org/10.1016/S0925-7535(00)00045-X
3.
BarshiI.DeganiA.MauroR.MumawR. J. (2024). Models of human-automation systems: Initial analysis of the boeing 737max design. In Proceedings of the HFES annual meeting (pp. 835–840, Vol. 68). SAGE. https://doi.org/10.1177/10711813241279805
4.
BhattacharyyaS.DavisJ.GuptaA.NarayanN.MatessaM. (2021). Assuring increasingly autonomous systems in human-machine teams: An urban air mobility case study. In FarrellM.LuckcuckM. (Eds.), Third workshop on formal methods for autonomous systems (FMAS 2021) (pp. 150–166, Vol. 348). Electronic Proceedings in Theoretical Computer Science. https://doi.org/10.4204/EPTCS.348.11
5.
BhattacharyyaS.EskridgeT. C.NeogiN. A.CarvalhoM.StaffordM. (2018). Formal assurance for cooperative intelligent autonomous agents. In LNCS (pp. 20–36, Vol. 10811). Springer. https://doi.org/10.1007/978-3-319-77935-5·2
6.
BoltonM. L. (2017). Novel developments in formal methods for human factors engineering. In Proceedings of the HFES annual meeting (pp. 715–717, Vol. 61). Sage. https://doi.org/10.1177/1541931213601664
7.
BrännströmA. (2025). Formal methods for verification in human-agent interaction [Doctoral dissertation, Umeå University].
8.
CamposJ. C.HarrisonM. D. (2025). Formal approaches for interactive systems. In VanderdoncktJ.PalanqueP.WincklerM. (Eds.), Handbook of human computer interaction (pp. 1–28). Springer Nature Switzerland. https://doi.org/10.1007/978-3-319-27648-9·120-1
9.
ClarkeE. M.GrumbergO.PeledD. A. (1999). Model checking. MIT Press.
10.
CubuktepeM.TopcuU. (2017). Intent prediction in shared control with delayed feedback. In Proceedings of the HFES annual meeting (pp. 733–734, Vol. 61). SAGE. https://doi.org/10.1177/1541931213601668
11.
DixA. (2023). Modelling interactions: Digital and physical. In CeroneA. (Ed.), Formal methods for an informal world: Ictac 2021 summer school, virtual event, astana, kazakhstan, september 1–7, 2021, tutorial lectures (pp. 1–29). Springer International Publishing. https://doi.org/10.1007/978-3-031-43678-9·1
12.
FerrariA.BeekM. H. T. (2022). Formal methods in railways: A systematic mapping study. ACM Computing Surveys, 55(4), Article 69. https://doi.org/10.1145/3520480
13.
GaneriwalaP.MatessaM.BhattacharyyaS.JonesR. M.DavisJ.KaurP.RolliniS. F.NeogiN. (2025). Design and validation of learning aware hmi for learning-enabled increasingly autonomous systems. In Proceedings of SysCon 2025. IEEE. https://doi.org/10.48550/arXiv.2501.18506
HenselC.JungesS.KatoenJ.-P.QuatmannT.VolkM. (2022). The probabilistic model checker storm. International Journal on Software Tools for Technology Transfer, 24(4), 589–610. https://doi.org/10.1007/s10009-021-00633-z
16.
KwiatkowskaM.NormanG.ParkerD. (2011). PRISM 4.0: Verification of probabilistic real-time systems. In BaierC.TinelliC. (Eds.), Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14–20, 2011, Proceedings, Part 23 (pp. 585–591). Springer.
17.
LangenfeldV.WestphalB.AlbrechtR.PodelskiA. (2018). But does it really do that? Using formal analysis to ensure desirable ACT-R model behaviour. In Proceedings of the Annual Meeting of the Cognitive Science Society (Vol. 40). Cognitive Science Society. https://escholarship.org/uc/item/3hg423jb
18.
LeeD.-A.SungS.YooJ.KimD.-H. (2012). Formal modeling and verification of operational flight program in a small-scale unmanned helicopter. Journal of Aerospace Engineering, 25(4), 530–540.
19.
MaL. M.FeighK. M. (2017). Jumpstarting modelling systems design: A generalized xml abstraction of simulation model. In Proceedings of the HFES annual meeting (pp. 718–722, Vol. 61). SAGE. https://doi.org/10.1177/1541931213601665
20.
NarayanN.GaneriwalaP.JonesR. M.MatessaM.BhattacharyyaS.DavisJ.PurohitH.RolliniS. F. (2023). Assuring learning-enabled increasingly autonomous systems. In 2023 IEEE International Systems Conference (SysCon) (pp. 1–7). IEEE. https://doi.org/10.1109/SysCon53073.2023.10131227
21.
NewcombeC.RathT.ZhangF.MunteanuB.BrookerM.DeardeuffM. (2015). How amazon web services uses formal methods. Commun. ACM, 58(4), 66–73. https://doi.org/10.1145/2699417
22.
O’ConnorM.TangiralaS.KumarR.BhattacharyyaS.SznaierS.HollowayL. (2006). A bottom-up approach to verification of hybrid model-based hierarchical controllers with application to underwater vehicles. In 2006 American Control Conference (pp. 1–6). IEEE. https://doi.org/10.1109/ACC.2006.1657389
23.
PaassenM. M. v.BoltonM. L.JiménezN. (2014). Checking formal verification models for human-automation interaction. In 2014 IEEE International Conference on Systems, Man, and Cybernetics (SMC) (pp. 3709–3714). IEEE. https://doi.org/10.1109/SMC.2014.6974507
24.
RoggenbachM.CeroneA.SchlingloffB.-H.SchneiderG.ShaikhS. A. (2022). Correction to: Formal methods for software engineering. In Formal methods for software engineering: Languages, methods, application domains (pp. C1–C1). Springer International Publishing. https://doi.org/10.1007/978-3-030-38800-3·10
25.
RushbyJ. (1997). Formal methods and their role in the certification of critical systems. In ShawR. (Ed.), Industrial safety and systems reliability (pp. 1–19). Springer. https://doi.org/10.1007/978-1-4471-0921-1_1
26.
Tavolato-WötzlC.TavolatoP. (2023). Enhancing trust in machine learning systems by formal methods. In Machine learning and knowledge extraction (pp. 170–187). Springer.
27.
ter BeekM. H.ChapmanR.CleavelandR.GaravelH.GuR.ter HorstI.KeirenJ. J.LecomteT.LeuschelM.RozierK. Y. (2024). Formal methods in industry. Formal Aspects of Computing, 37(1), 1–38.
28.
TuckerJ. V. (2022). Origins and development of formal methods. In Formal methods for software engineering: Languages, methods, application domains (pp. 455–488). Springer International Publishing. https://doi.org/10.1007/978-3-030-38800-3_9
WingJ. M. (1990). A specifier’s introduction to formal methods. Computer, 23(9), 8–22.
32.
WoodcockJ.LarsenP. G.BicarreguiJ.FitzgeraldJ. (2009). Formal methods: Practice and experience. ACM Computing Surveys, 41(4), 1–36. https://doi.org/10.1145/1592434.1592436
33.
ZhengX.BoltonM. L.DalyC.FengL. (2017). A formal human reliability analysis of a community pharmacy dispensing procedure. In Proceedings of the HFES annual meeting (pp. 728–732, Vol. 61). SAGE. https://doi.org/10.1177/1541931213601667
