In this paper, we present a methodology for describing crop models that combines agronomic knowledge with formal descriptions typical of computer science. Our aim is to provide crop modeling researchers with a formal methodology, supported by automatic tools, enabling the simulation of biological systems at different scales, from individual plants to entire populations, under heterogeneous growth conditions. To validate our approach, we used the well-known tomato model TOMGRO as a case study, rewriting it in the formal language of Discrete-Time Hybrid Automata (DTHA). We then automatically generated a correct-by-construction software version of the model, scalable to grids of multiple plants, as an executable program simulating plant growth under different microclimatic conditions. We tested the scalability of this approach for increasing grid sizes ranging from 9 to 1600 plants, and reported experimental data on the time required to synthesize and run the simulation program.
A formal approach to crop modeling: Automatic code generation and grid simulation using finite state automata / Brentarolli, E., Quaglia, D., Benvenuti, L., Villa, T., Massa, D., Battista, P., Rapi, B., Incrocci, L.. - In: COMPUTERS AND ELECTRONICS IN AGRICULTURE. - ISSN 0168-1699. - 255:(2026). [10.1016/j.compag.2026.112367]
A formal approach to crop modeling: Automatic code generation and grid simulation using finite state automata
Benvenuti, Luca;Villa, Tiziano;
2026
Abstract
In this paper, we present a methodology for describing crop models that combines agronomic knowledge with formal descriptions typical of computer science. Our aim is to provide crop modeling researchers with a formal methodology, supported by automatic tools, enabling the simulation of biological systems at different scales, from individual plants to entire populations, under heterogeneous growth conditions. To validate our approach, we used the well-known tomato model TOMGRO as a case study, rewriting it in the formal language of Discrete-Time Hybrid Automata (DTHA). We then automatically generated a correct-by-construction software version of the model, scalable to grids of multiple plants, as an executable program simulating plant growth under different microclimatic conditions. We tested the scalability of this approach for increasing grid sizes ranging from 9 to 1600 plants, and reported experimental data on the time required to synthesize and run the simulation program.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.


