In Silico Clinical Trials (ISCT), i.e. clinical experimental campaigns carried out by means of computer simulations, hold the promise to decrease time and cost for the safety and efficacy assessment of pharmacological treatments, reduce the need for animal and human testing, and enable precision medicine. In this paper we present methods and an algorithm that, by means of extensive computer simulation-based experimental campaigns (ISCT) guided by intelligent search, optimise a pharmacological treatment for an individual patient (precision medicine). We show the effectiveness of our approach on a case study involving a real pharmacological treatment, namely the downregulation phase of a complex clinical protocol for assisted reproduction in humans.

The goal of System Level Formal Verification is to show system correctness notwithstanding uncontrollable events (disturbances), as for example faults, variations in system parameters, external inputs, etc. This may be achieved with an exhaustive Hardware In the Loop Simulation based approach, by c onsidering all relevant scenarios in the System Under Verification (SUV) operational environment. In this paper, we present SyLVaaS, a Web-based tool enabling Verification as a Service (VaaS). SyLVaaS implements an assume-guarantee approach to (Hardware In the Loop Simulation based) System Level Formal Verification. SyLVaaS takes as input a finite state automaton defining the SUV operational environment and computes, using parallel algorithms deployed in a cluster infrastructure, a set of highly optimised simulation campaigns, which can be executed in an embarrassingly parallel fashion (i.e., with no communication among the parallel processes) on a set of Simulink instances, using a platform independent Simulink driver downloadable from the SyLVaaS Web site. As the actual simulation is carried out at the user premises (e.g., on a private cluster), SyLVaaS allows full Intellectual Property protection of the SUV model as well as of the user verification flow. The simulation campaigns computed by SyLVaaS randomise the verification order of operational scenarios and this enables, at anytime during the parallel simulation activity, the estimation of the completion time and the computation of an upper bound to the Omission Probability, i.e., the probability that there is a yet-to-be-simulated operational scenario which violates the property under verification. This information supports graceful degradation in the verification activity. We show effectiveness of the SyLVaaS algorithms and infrastructure by evaluating the system on case studies consisting of input operational environments entailing up to 35 641 501 scenarios related to the system level verification of models from the Simulink distribution (namely, Inverted Pendulum on a Cart and Fuel Control System).

The SmartHG project goal is to develop a suite of integrated software services (the SmartHG Platform) aiming at steering residential users energy demand in order to: keep operating conditions of the electrical grid within given healthy bounds, minimize energy costs, and minimize CO2 emissions. This is achieved by exploiting knowledge (demand awareness) of electrical energy prosumption of residential users as gained from SmartHG sensing and communication infrastructure. This paper describes such an infrastructure along with user demand patterns emerging from the data gathered from ~600 sensors installed in ~40 homes participating in SmartHG test-beds.

In order to optimally manage a modern electricity distribution network, peaks in residential users demand should be avoided, as this can reduce energy and network asset management costs. Furthermore, this must be done without compressing residential users demand. To this aim, in a demand response setting, residential users are given a price policy, which economically motivates them to shift their loads in order to achieve this goal. However, if the price policy for all users is similar, this demand response may result in simply shifting the demand peaks (peak rebound), leaving the problem unsolved. In this paper we propose a novel methodology which i) for each network substation s, automatically computes the desired power profile to be kept in order to optimally manage the network itself, ii) for each network substation s, automatically synthesizes individualized price policies for residential users connected to s, so that s is kept at the desired profile. Note that price policies individualization avoids the peak rebound problem, as different users have different low tariff areas. Furthermore, our methodology measures the flexibility of a residential user as the capacity needed by a home energy storage system (e.g., a battery) to always follow the given price policy, thus mitigating residential users discomfort. We show the feasibility of our approach on a realistic scenario taken from an existing medium voltage Danish distribution network.

The goal of System Level Formal Verification is to show system correctness notwithstanding uncontrollable events (disturbances), as for example faults, variation in system parameters, external inputs, etc. This may be achieved with an exhaustive Hardware In the Loop Simulation based approach, by considering all relevant scenarios in the System Under Verification (SUV) operational environment. In this paper, we present SyLVaaS, a Web-based tool enabling Verification as a Service (VaaS). SyLVaaS implements an assume-guarantee approach to the verification problem outlined above. SyLVaaS takes as input a high-level model defining the SUV operational environment and computes, using parallel algorithms deployed in a cluster infrastructure, a set of highly optimised simulation campaigns, which can be executed in an embarrassingly parallel fashion on a set of Simulink instances, using a platform independent Simulink driver downloadable from the SyLVaaS Web site. As the actual simulation is carried out at the user premises (e.g., in a private cluster), SyLVaaS allows full Intellectual Property protection on the SUV model and the user verification flow. The simulation campaigns computed by SyLVaaS randomise the verification order of operational scenarios and this enables, at anytime during the parallel simulation activity, the estimation of the completion time and the computation of an upper bound to the Omission Probability, i.e., the probability that there is a yet-to-be-simulated operational scenario which violates the property under verification. This information supports graceful degradation in the verification activity. We show effectiveness of the SyLVaaS algorithms and infrastructure by evaluating the system on industry-scale input related to the verification of the Fuel Control System (FCS) model in the Simulink distribution.

We present a parallel random exhaustive Hardware In the Loop Simulation based model checker for hybrid systems that, by simulating all operational scenarios exactly once in a uniform random order, is able to provide, at any time during the verification process, an upper bound to the probability that the System Under Verification exhibits an error in a yet-to-be-simulated scenario (Omission Probability). We show effectiveness of the proposed approach by presenting experimental results on System Level Formal Verification of the Fuel Control System example in the Simulink distribution. To the best of our knowledge, no previously published model checker can exhaustively verify hybrid systems of such a size and provide at any time an upper bound to the Omission Probability.

One of the main goals of systems biology models in a health-care context is to individualise models in order to compute patient-specific predictions for the time evolution of species (e.g., hormones) concentrations. In this paper we present a statistical model checking based approach that, given an inter-patient model and a few clinical measurements, computes a value for the model parameter vector (model individualisation) that, with high confidence, is a global minimum for the function evaluating the mismatch between the model predictions and the available measurements. We evaluate effectiveness of the proposed approach by presenting experimental results on using the GynCycle model (describing the feedback mechanisms regulating a number of reproductive hormones) to compute patient-specific predictions for the time evolution of blood concentrations of E2 (Estradiol), P4 (Progesterone), FSH (Follicle-Stimulating Hormone) and LH (Luteinizing Hormone) after a certain number of clinical measurements.

The goal of System Level Formal Verification (SLFV) is to show system correctness notwithstanding uncontrollable events (such as: faults, variation in system parameters, external inputs, etc). Hardware In the Loop Simulation (HILS) based SLFV attains such a goal by considering exhaustively all relevant simulation scenarios. We present a distributed multi-core algorithm for HILS-based SLFV. Our experimental results on the Fuel Control System example in the Simulink distribution show that by using 64 machines with an 8 core processor each we can complete the SLFV activity in about 27 hours whereas a sequential approach would require more than 200 days. To the best of our knowledge this is the first time that a distributed multi-core algorithm for HILS-based SLFV is presented.

Many embedded systems are indeed software-based control systems , that is, control systems whose controller consists of control software running on a microcontroller device. This motivates investigation on formal model-based design approaches for automatic synthesis of embedded systems control software. We present an algorithm, along with a tool QKS implementing it, that from a formal model (as a discrete-time linear hybrid system ) of the controlled system ( plant ), implementation specifications (that is, number of bits in the Analog-to-Digital , AD, conversion) and system-level formal specifications (that is, safety and liveness requirements for the closed loop system ) returns correct-by-construction control software that has a Worst-Case Execution Time (WCET) linear in the number of AD bits and meets the given specifications. We show feasibility of our approach by presenting experimental results on using it to synthesize control software for a buck DC-DC converter, a widely used mixed-mode analog circuit, and for the inverted pendulum.

Many Embedded Systems are indeed Software Based Control Systems (SBCSs), that is control systems whose controller consists of control software running on a microcontroller device. This motivates investigation on Formal Model Based Design approaches for control software. Given the formal model of a plant as a Discrete Time Linear Hybrid System and the implementation specifications (that is, number of bits in the Analog-to-Digital (AD) conversion) correct-by-construction control software can be automatically generated from System Level Formal Specifications of the closed loop system (that is, safety and liveness requirements), by computing a suitable finite abstraction of the plant.

The automation of power grids by means of supervisory control and data acquisition (SCADA) systems has led to an improvement of power grid operations and functionalities but also to pervasive cyber interdependencies between power grids and telecommunication networks. Many power grid services are increasingly depending upon the adequate functionality of SCADA system which in turn strictly depends on the adequate functionality of its communication infrastructure. We propose to tackle the SCADA risk analysis by means of different and heterogeneous modeling techniques and software tools. We demonstrate the applicability of our approach through a case study on an actual SCADA system for an electrical power distribution grid. The modeling techniques we discuss aim at providing a probabilistic dependability analysis, followed by a worst case analysis in presence of malicious attacks and a real-time performance evaluation.

We present a symbolic model checking algorithm for verification of Nash equilibria in finite state mechanisms modeling multiple administrative domains (MAD) distributed systems. Given a finite state mechanism, a proposed protocol for each agent and an indifference threshold for rewards, our model checker returns PASS if the proposed protocol is a Nash equilibrium (up to the given indifference threshold) for the given mechanism, FAIL otherwise. We implemented our model checking algorithm inside the NuSMV model checker and present experimental results showing its effectiveness for moderate size mechanisms.

We study the problem of optimal skip placement in an inverted list. Assuming the query distribution to be known in advance, we formally prove that an optimal skip placement can be computed quite efficiently. Our best algorithm runs in time O (n log n), n being the length of the list.