Verify Engineering Models, not Scientific Models

Author(s): Shaokai Lin and Edward A. Lee

Abstract
Driving progress in science and engineering for centuries, models are powerful tools for understanding systems and building abstractions. However, the goal of models in science is different from that in engineering, and we observe the misuse of models undermining research goals. Specifically in the field of formal methods, we advocate that verification should be performed on engineering models rather than scientific models, to the extent possible. We observe that models under verification are, very often, scientific models rather than engineering models, and we show why verifying scientific models is ineffective in engineering efforts. To guarantee safety in an engineered system, it is the engineering model one should verify. This model can be used to derive a correct-by-construction implementation. To demonstrate our proposed principle, we review lessons learned from verifying programs in a language called Lingua Franca using Timed Rebeca.

Electronic Downloads

• https://doi.org/10.1007/978-3-031-85134-6_9

---

Citation Formats

• APA
  

                  
  Shaokai Lin and Edward A. Lee. (2025). Verify Engineering Models, not Scientific Models. In Rebeca for Actor Analysis in Action.  doi:10.1007/978-3-031-85134-6_9.                     
                  
                  

• MLA
  

                  
  Shaokai Lin and Edward A. Lee. "Verify Engineering Models, not Scientific Models." Rebeca for Actor Analysis in Action, 2025.  doi:10.1007/978-3-031-85134-6_9.                     
                  
                  

• Chicago
  

                  
  Shaokai Lin and Edward A. Lee. "Verify Engineering Models, not Scientific Models." Rebeca for Actor Analysis in Action, 2025.  doi:10.1007/978-3-031-85134-6_9.                     
                  
                  

• BibTeX
  

                      
  @inproceedings{LinLee:25:Verify,
  	author = {Shaokai Lin and Edward A. Lee},
  	title = {Verify Engineering Models, not Scientific Models},
  	booktitle = {Rebeca for Actor Analysis in Action},
  	volume = {LNCS 15560},
  	year = {2025},
  	doi = {10.1007/978-3-031-85134-6_9},
  	abstract = {Driving progress in science and engineering for centuries, models are powerful tools for understanding systems and building abstractions. However, the goal of models in science is different from that in engineering, and we observe the misuse of models undermining research goals. Specifically in the field of formal methods, we advocate that verification should be performed on engineering models rather than scientific models, to the extent possible. We observe that models under verification are, very often, scientific models rather than engineering models, and we show why verifying scientific models is ineffective in engineering efforts. To guarantee safety in an engineered system, it is the engineering model one should verify. This model can be used to derive a correct-by-construction implementation. To demonstrate our proposed principle, we review lessons learned from verifying programs in a language called Lingua Franca using Timed Rebeca.},
  	URL = {https://doi.org/10.1007/978-3-031-85134-6_9}}