2015 · 17 citations · 16 references
Software MaintenanceSoftware Development PracticeEngineeringCompiler TechnologyVerificationSoftware EngineeringSoftware ProcessFormal VerificationSoftware AnalysisSystems EngineeringProgram TransformationSoftware PracticeModel Transformation LanguageSoftware ModernizationSoftware Development ProcessDesignComputer EngineeringComputer ScienceSoftware DesignCode RefactoringSoftware EvolutionSoftware Modernization TransformationProgram AnalysisSoftware TestingFormal MethodsDesign ThinkingC++ CodeProgram SynthesisLegacy CodeSystem Software
Software modernization often involves complex code transformations that convert legacy code to new architectures or platforms, while preserving the semantics of the original programs. We present the lessons learnt from an industrial software modernization project of considerable size. This includes collecting requirements for a code-to-model transformation, designing and implementing the transformation algorithm, and then validating correctness of this transformation for the code-base at hand. Our transformation is implemented in the TXL rewriting language and assumes specifically structured C++ code as input, which it translates to a declarative configuration model. The correctness criterion for the transformation is that the produced model admits the same configurations as the input code. The transformation converts C++ functions specifying around a thousand configuration parameters. We verify the correctness for each run individually, using translation validation and symbolic execution. The technique is formally specified and is applicable automatically for most of the code-base.
16
Symbolic execution and program testing
James C. King · Communications of the ACM · 1976 · 2.9K citations · Full text
ATL: A model transformation tool
Frédéric Jouault, Freddy Allilaire, Jean Bézivín et al. · Science of Computer Programming · 2008 · 955 citations
Why Do Computers Stop and What Can Be Done About It?
Jim Gray · 2024 · 671 citations