Abstract:This paper presents a formal approach to specify and verify object-oriented programs written in the `programming to interfaces' paradigm. In this approach, besides the methods to be invoked by its clients, an interface also declares a set of abstract and polymorphic function/predicate symbols, together with a set of constraints about these symbols. The methods declared in this interface are specified using these abstract symbols. A class implementing this interface can give its own definitions to the abstract symbols, as long as all the constraints are satisfied. This class implements all the methods declared in the interface such that the method specification declared in the interface are satisfied w.r.t. the function symbol definitions in this class. Based on the constraints about the abstract symbols, client code using the interfaces can be specified and verified precisely without knowing what classes implement the interfaces. Given more information about the implementing classes, the specifications of the client code can be specialized into more precise ones without re-verifying the client code.

Abstract:Statistical Model Checking (SMC), as a technique to mitigate the issue of state space explosion in numerical probabilistic model checking, can efficiently obtain an approximate result with an error bound by statistically analysing the simulation traces. SMC however may become very time consuming due to the generation of an extremely large number of traces in some cases. Improving the performance of SMC effectively is still a challenge. To solve the problem, we propose an optimized SMC approach called AL-SMC which effectively reduces the required sample traces, thus to improve the performance of SMC by automatic abstraction and learning. First, we present property-based trace abstraction for simplifying the cumbersome traces drawn from the original model. Second, we learn the analysis model called Prefix Frequency Tree (PFT) from the abstracted traces, and optimize the PFT using the two-phase reduction algorithm. By means of the optimized PFT, the original probability space is partitioned into several sub-spaces on which we evaluate the probabilities parallelly in the final phase. Besides, we analyse the core algorithms in terms of time and space complexity, and implement AL-SMC in our Modana Platform to support the automatic process. Finally we discuss the experiment results for the case study :energy-aware building which shows that the number of sample traces is effectively reduced (by nearly 20\% to 50\%) while ensuring the accuracy of the result with an acceptable error.

Abstract:The full combination of if-expression and subtyping was known as a challenging problem for a long time. The difficulty comes from the fact that two branches of an if-expression might have different types and these types might not have a unique least upper bound. Such situation could happen in real object oriented languages such as Java. In our previous work, we investigated this problem in a simply typed lambda calculus extended with subtyping and if-expression and solved the type checking problem in that system. In this paper, we extend the result to bounded quantification combined with if-expression.

Abstract:The appraisal of the status quo for the methods of evaluating model transformation languages (MTLs) manifests several shortcomings: they are often either language-specific or feature-specific, they may lack of sufficient discussion on possible values for proposed criteria, few MTLs may be applied in their evaluation, or a combination of these limitations. We have previously proposed a method which utilizes programming language (PL) criteria for evaluation of MTLs. In this paper, an improved method is proposed in which a large family of 11 major criteria with total of 46 sub-criteria, mainly inspired from PL evaluation criteria, is used to evaluate MTLs. Then, an interactive methodology is proposed that consolidates the criteria to establish a \textit{decision-support} system for MTL selection. In order to investigate the effectiveness of the criteria and the proposed methodology, six MTLs were used for studies: ATL, Kermeta, ETL, QVT-O, QVT-R, and TGG. The results of MTL evaluations corroborate that the criteria are highly effective in practice; they provide helpful insights for different users to enable them to choose the most appropriate MTL for the application at hand. With our decision-support methodology, we could have achieved evidence to imply applicability in real-world scenarios.