Program specialization is mainly recognized as a powerful technique for optimizing software systems. Nonetheless, it can also be productively employed in other application areas. This paper presents an assertion-guided program specialization methodology for efficiently imposing safety properties on software systems. The program specializer takes as input a set A of logical assertions that specifies the expected system behavior plus a software system that is modeled as a Maude program R that may violate some of the assertions in A. The outcome is a safe refinement R▹ of R in which every system computation is a good run of R, i.e., it satisfies the assertions in A. The specialization technique has been fully automated in the ÁTAME system and ensures that no good run of R is removed from R▹, while the number of bad runs is reduced to zero. The efficiency and scalability of our technique is empirically demonstrated by means of a thorough experimental evaluation of the ÁTAME system, which shows fast specialization times and good performance of the computed specializations, even for large assertion sets.
Efficient Safety Enforcement for Maude Programs via Program Specialization in the ÁTAME System
Ballis D.
;
2020-01-01
Abstract
Program specialization is mainly recognized as a powerful technique for optimizing software systems. Nonetheless, it can also be productively employed in other application areas. This paper presents an assertion-guided program specialization methodology for efficiently imposing safety properties on software systems. The program specializer takes as input a set A of logical assertions that specifies the expected system behavior plus a software system that is modeled as a Maude program R that may violate some of the assertions in A. The outcome is a safe refinement R▹ of R in which every system computation is a good run of R, i.e., it satisfies the assertions in A. The specialization technique has been fully automated in the ÁTAME system and ensures that no good run of R is removed from R▹, while the number of bad runs is reduced to zero. The efficiency and scalability of our technique is empirically demonstrated by means of a thorough experimental evaluation of the ÁTAME system, which shows fast specialization times and good performance of the computed specializations, even for large assertion sets.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
