\n \n \n
\n
\n\n \n \n \n \n \n \n Verifying ParamGen: A case study in scientific software abstraction and modeling.\n \n \n \n \n\n\n \n Altuntas, A.; Baugh, J.; and Nusbaumer, J.\n\n\n \n\n\n\n In
Proceedings of the 2023 Improving Scientific Software Conference, pages 1-9, 2023. \n
(No. NCAR/TN-576+PROC)\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 8 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inproceedings{altuntas-iss-2023,\ntitle = {Verifying {ParamGen}: A case study in scientific software abstraction and modeling},\nauthor = {Altuntas, Alper and Baugh, John and Nusbaumer, Jesse},\nbooktitle = {Proceedings of the 2023 Improving Scientific Software Conference},\nnote = {{(No.~NCAR/TN-576+PROC)}},\nyear = {2023},\npages = {1-9},\nurl_pdf = {papers/altuntas-iss-2023.pdf},\ndoi = {10.5065/j0e4-ss70},\nabstract = {\nWe introduce ParamGen, an infrastructure library for climate models to\ngenerate input files that specify physics, parameterizations, and\nother behavior. ParamGen supports arbitrary Python expressions for\nspecifying a default set of runtime parameters and values, thereby\nproviding a high level of expressiveness and flexibility. Initially\ndeveloped for the MOM6 ocean component in Community Earth System Model\n(CESM), ParamGen is now used by several additional CESM\ncomponents. Therefore, it is of high importance that it operates\ncorrectly, i.e., absent any undesired and unexpected behavior. To that\nend, we develop an abstract verification model of ParamGen in Alloy, a\nsoftware modeling and analysis tool with a declarative language that\ncombines first-order logic and relational calculus. We evaluate the\ncorrectness of ParamGen via Alloy and discuss how abstract models and\nformal verification can help quickly frame questions and get answers\nregarding the structure and behavior of our scientific computing\napplications. We also describe our experience in coming to a cleaner\nand well-formed software design and abstractions as a result of the\nmodeling exercise we present in this study.}\n}\n\n
\n
\n\n\n
\n We introduce ParamGen, an infrastructure library for climate models to generate input files that specify physics, parameterizations, and other behavior. ParamGen supports arbitrary Python expressions for specifying a default set of runtime parameters and values, thereby providing a high level of expressiveness and flexibility. Initially developed for the MOM6 ocean component in Community Earth System Model (CESM), ParamGen is now used by several additional CESM components. Therefore, it is of high importance that it operates correctly, i.e., absent any undesired and unexpected behavior. To that end, we develop an abstract verification model of ParamGen in Alloy, a software modeling and analysis tool with a declarative language that combines first-order logic and relational calculus. We evaluate the correctness of ParamGen via Alloy and discuss how abstract models and formal verification can help quickly frame questions and get answers regarding the structure and behavior of our scientific computing applications. We also describe our experience in coming to a cleaner and well-formed software design and abstractions as a result of the modeling exercise we present in this study.\n
\n\n\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Automatic modelling and verification of Autosar architectures.\n \n \n \n \n\n\n \n Zhang, M.; Teng, Y.; Kong, H.; Baugh, J.; Su, Y.; Mi, J.; and Du, B.\n\n\n \n\n\n\n
Journal of Systems and Software, 201: 111675. 2023.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 10 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@article{zhang-jss-2023,\nauthor = {Zhang, Miaomiao and Teng, Yu and Kong, Hui and Baugh, John and Su, Yu and Mi, Junri and Du, Bowen},\ntitle = {Automatic modelling and verification of {Autosar} architectures},\njournal = {Journal of Systems and Software},\nvolume = {201},\npages = {111675},\nyear = {2023},\ndoi = {10.1016/j.jss.2023.111675},\npublisher = {Elsevier},\nurl_pdf = {papers/zhang-jss-2023.pdf},\nkeywords = {Vehicle electronic system, Autosar, formal modelling, timed\n automata, verification},\nabstract = {\nAutosar (AUTomotive Open System ARchitecture) is a development\npartnership whose primary goal is the standardization of basic system\nfunctions and functional interfaces for electronic control units in\nautomobiles. As an open specification, its layered software\narchitecture promotes the interoperability of real-time embedded\nvehicle systems and components. It also opens up the possibility of\nformal modelling and verification approaches, centred around the\nspecification, that can be used to support analysis in the early\nstages of design. In this paper, we describe a methodology and\nassociated tool, called A2A, that automatically models systems defined\nby the Autosar specifications as timed automata, and then verifies\ntheir timing properties using Uppaal. It contains 22 groups of timed\nautomata templates, together with two auxiliary test templates, that\nmodel the Autosar architecture and timing properties, allowing\ntime-related behaviours to be extracted from the three-layer\narchitecture, i.e., the Autosar Software, Autosar Runtime Environment,\nand Basic Software layers, and templates to be automatically\ninstantiated. The timing properties are specified using timed\ncomputation tree logic (TCTL) in Uppaal to verify the system model. We\ndemonstrate the capabilities of the methodology by applying it to an\nAutosar architecture that describes an internal vehicle light control\nsystem, thereby showing its effectiveness.}\n}\n\n
\n
\n\n\n
\n Autosar (AUTomotive Open System ARchitecture) is a development partnership whose primary goal is the standardization of basic system functions and functional interfaces for electronic control units in automobiles. As an open specification, its layered software architecture promotes the interoperability of real-time embedded vehicle systems and components. It also opens up the possibility of formal modelling and verification approaches, centred around the specification, that can be used to support analysis in the early stages of design. In this paper, we describe a methodology and associated tool, called A2A, that automatically models systems defined by the Autosar specifications as timed automata, and then verifies their timing properties using Uppaal. It contains 22 groups of timed automata templates, together with two auxiliary test templates, that model the Autosar architecture and timing properties, allowing time-related behaviours to be extracted from the three-layer architecture, i.e., the Autosar Software, Autosar Runtime Environment, and Basic Software layers, and templates to be automatically instantiated. The timing properties are specified using timed computation tree logic (TCTL) in Uppaal to verify the system model. We demonstrate the capabilities of the methodology by applying it to an Autosar architecture that describes an internal vehicle light control system, thereby showing its effectiveness.\n
\n\n\n
\n\n\n
\n\n\n\n\n\n