Quality Attributes and Preferences on the Synthesis of Reactive Systems

EZEQUIEL GUSTAVO CASTELLANO

Ciudad Autónoma Buenos Aires

Simposio; ICSE 2017 PhD and Young Researchers Warmup Symposium; 2016

Given a model of the environment?s behaviour, a set of system goals and a set of controllable actions, the controllersynthesis problem is to automatically generate a controller that only restricts controllable actions. Qualitative controlproblems are boolean in the sense that a controller guarantees a set of goals, or it does not. However, several solutionsmay be allowed applying different strategies to satisfy the goals. Current approaches do not allowexpressing preferences. Hence, the obtained solution is accidental to the way the controller synthesis technique isimplemented.Requirements Engineering distinguish between hard and soft goals (i.e.: preferences). Quantitative synthesistechniques are a natural way of optimising control with respect to preferences, however, they requirequantitative modelling, which in many cases is not available, possible or desired, and incur in high computationalcomplexity.As a first step, we restrict our attention to reachability goals and reduced-latency preference. We believe thata qualitative approach is of interest, since there are scenarios where time durations of activities are not knownin advance, nonetheless, there are solutions that might be preferable regarding the quantitative durations. Time isreasoned upon symbolically, thus relieving the user from providing concrete quantitative measures. We developeda formal approach to reason about time symbolically and fairly compare controllers using schedulers and PTAsemantics, and provide approximations to produce controllers that aim to reduce latency for reachability goals. Weevaluate our approach on a number of case studies using an extension of the MTSA tool that supports SMTqueries using Z3.Dealing with relations between activity durations is part of our future work. Additionally, we would like todeal with more expressive goals, such as GR(1), which has a central challenge: dealing with cycles productof uncontrollable behaviour. Moreover, we want to explore other kind of preferences such as maximisation ofconcurrency or minimisation of resource usage. However, this will require dealing with goals prioritisation.