Specification, refinement and verification of concurrent systems - An integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of modelling complex data structures needed to define the component processes of such systems, and CSP enables the concise specification of process interactions. The basis of the integration is a semantics of Object-Z classes identical to that of CSP processes. This allows classes specified in Object-Z to he used directly within the CSP part of the specification. In addition to specification, we also discuss refinement and verification in this model. The common semantic basis enables a unified method of refinement to be used, based upon CSP refinement. To enable state-based techniques to be used fur the Object-Z components of a specification we develop state-based refinement relations which are sound and complete with respect to CSP refinement. In addition, a verification method for static and dynamic properties is presented. The method allows us to verify properties of the CSP system specification in terms of its component Object-Z classes by using the laws of the the CSP operators together with the logic for Object-Z.

Structural refinement of systems specified in object-z and CSP

This paper is concerned with methods for refinement of specifications written using a combination of Object-Z and CSP. Such a combination has proved to be a suitable vehicle for specifying complex systems which involve state and behaviour, and several proposals exist for integrating these two languages. The basis of the integration in this paper is a semantics of Object-Z classes identical to CSP processes. This allows classes specified in Object-Z to be combined using CSP operators. It has been shown that this semantic model allows state-based refinement relations to be used on the Object-Z components in an integrated Object-Z/CSP specification. However, the current refinement methodology does not allow the structure of a specification to be changed in a refinement, whereas a full methodology would, for example, allow concurrency to be introduced during the development life-cycle. In this paper, we tackle these concerns and discuss refinements of specifications written using Object-Z and CSP where we change the structure of the specification when performing the refinement. In particular, we develop a set of structural simulation rules which allow single components to be refined to more complex specifications involving CSP operators. The soundness of these rules is verified against the common semantic model and they are illustrated via a number of examples.

Wind-CSP short-term coordination by MILP approach

This paper is on the maximization of total profit in a day-ahead market for a price-taker producer needing a short-term scheduling for wind power plants coordination with concentrated solar power plants, having thermal energy storage systems. The optimization approach proposed for the maximization of profit is a mixed-integer linear programming problem. The approach considers not only transmission grid constraints, but also technical operating constraints on both wind and concentrated solar power plants. Then, an improved short-term scheduling coordination is provided due to the more accurate modelling presented in this paper. Computer simulation results based on data for the Iberian wind and concentrated solar power plants illustrate the coordination benefits and show the effectiveness of the approach.

Self-Scheduling for energy and spinning reserve of wind/CSP plants by a MILP approach

This paper is on the self-scheduling for a power producer taking part in day-ahead joint energy and spinning reserve markets and aiming at a short-term coordination of wind power plants with concentrated solar power plants having thermal energy storage. The short-term coordination is formulated as a mixed-integer linear programming problem given as the maximization of profit subjected to technical operation constraints, including the ones related to a transmission line. Probability density functions are used to model the variability of the hourly wind speed and the solar irradiation in regard to a negative correlation. Case studies based on an Iberian Peninsula wind and concentrated solar power plants are presented, providing the optimal energy and spinning reserve for the short-term self-scheduling in order to unveil the coordination benefits and synergies between wind and solar resources. Results and sensitivity analysis are in favour of the coordination, showing an increase on profit, allowing for spinning reserve, reducing the need for curtailment, increasing the transmission line capacity factor. (C) 2014 Elsevier Ltd. All rights reserved.

Wind-CSP short-term coordination by Milp approach

This paper is on the maximization of total profit in a day-ahead market for a price-taker producer needing a short-term scheduling for wind power plants coordination with concentrated solar power plants, having thermal energy storage systems. The optimization approach proposed for the maximization of profit is a mixed-integer linear programming problem. The approach considers not only transmission grid constraints, but also technical operating constraints on both wind and concentrated solar power plants. Then, an improved short-term scheduling coordination is provided due to the more accurate modelling presented in this paper. Computer simulation results based on data for the Iberian wind and concentrated solar power plants illustrate the coordination benefits and show the effectiveness of the approach.

Optimal generation scheduling of wind-CSP systems in day-ahead electricity markets

This paper presents a coordination approach to maximize the total profit of wind power systems coordinated with concentrated solar power systems, having molten-salt thermal energy storage. Both systems are effectively handled by mixed-integer linear programming in the approach, allowing enhancement on the operational during non-insolation periods. Transmission grid constraints and technical operating constraints on both systems are modeled to enable a true management support for the integration of renewable energy sources in day-ahead electricity markets. A representative case study based on real systems is considered to demonstrate the effectiveness of the proposed approach. © IFIP International Federation for Information Processing 2015.

RTS,S/AS02A malaria vaccine does not induce parasite CSP T cell epitope selection and reduces multiplicity of infection

Objective: The candidate malaria vaccine RTS,S/AS02A is a recombinant protein containing part of the circumsporozoite protein (CSP) sequence of Plasmodium falciparum, linked to the hepatitis B surface antigen and formulated in the proprietary adjuvant system AS02A. In a recent trial conducted in children younger than age five in southern Mozambique, the vaccinedemonstrated significant and sustained efficacy against both infection and clinical disease. In a follow-up study to the main trial, breakthrough infections identified in the trial were examined to determine whether the distribution of csp sequences was affected by the vaccine and to measure the multiplicity of infecting parasite genotypes. Design: P. falciparum DNA from isolates collected during the trial was used for genotype studies. Setting: The main trial was carried out in the Manhiça district, Maputo province, Mozambique, between April 2003 and May 2004. Participants: Children from the two cohorts of the main trial provided parasite isolates as follows: children from Cohort 1 who were admitted to hospital with clinical malaria; children from Cohort 1 who were parasite-positive in a cross-sectional survey at study month 8.5; children from Cohort 2 identified as parasite-positive during follow-up by active detection of infection. Outcome: Divergence of DNA sequence encoding the CSP T cell-epitope region sequence from that of the vaccine sequence was measured in 521 isolates. The number of distinct P. falciparum genotypes was also determined. Results: We found no evidence that parasite genotypes from children in the RTS,S/AS02A arm were more divergent than those receiving control vaccines. For Cohort 1 (survey at studymonth 8.5) and Cohort 2, infections in the vaccine group contained significantly fewer genotypes than those in the control group, (p 1/4 0.035, p 1/4 0.006), respectively, for the two cohorts. This was not the case for children in Cohort 1 who were admitted to hospital (p 1/4 0.478). Conclusions: RTS,S/AS02A did not select for genotypes encoding divergent T cell epitopes in the C-terminal region of CSP in this trial. In both cohorts, there was a modest reduction in the mean number of parasite genotypes harboured by vaccinated children compared with controls, but only among those with asymptomatic infections.

Virosome-Formulated Plasmodium falciparum AMA-1 & CSP Derived Peptides as Malaria Vaccine: Randomized Phase 1b Trial in Semi-Immune Adults & Children.

Background: This trial was conducted to evaluate the safety and immunogenicity of two virosome formulated malaria peptidomimetics derived from Plasmodium falciparum AMA-1 and CSP in malaria semi-immune adults and children.Methods: The design was a prospective randomized, double-blind, controlled, age-deescalating study with two immunizations. 10 adults and 40 children (aged 5-9 years) living in a malaria endemic area were immunized with PEV3B or virosomal influenza vaccine Inflexal (R) V on day 0 and 90.Results: No serious or severe adverse events (AEs) related to the vaccines were observed. The only local solicited AE reported was pain at injection site, which affected more children in the Inflexal (R) V group compared to the PEV3B group (p = 0.014). In the PEV3B group, IgG ELISA endpoint titers specific for the AMA-1 and CSP peptide antigens were significantly higher for most time points compared to the Inflexal (R) V control group. Across all time points after first immunization the average ratio of endpoint titers to baseline values in PEV3B subjects ranged from 4 to 15 in adults and from 4 to 66 in children. As an exploratory outcome, we found that the incidence rate of clinical malaria episodes in children vaccinees was half the rate of the control children between study days 30 and 365 (0.0035 episodes per day at risk for PEV3B vs. 0.0069 for Inflexal (R) V; RR = 0.50 [95%-CI: 0.29-0.88], p = 0.02).Conclusion: These findings provide a strong basis for the further development of multivalent virosomal malaria peptide vaccines.

CSP-A Model for In Vivo Presentation of Plasmodium berghei Sporozoite Antigens by Hepatocytes.

One target of protective immunity against the Plasmodium liver stage in BALB/c mice is represented by the circumsporozoite protein (CSP), and mainly involves its recognition by IFN-γ producing specific CD8+T-cells. In a previous in vitro study we showed that primary hepatocytes from BALB/c mice process Plasmodium berghei (Pb) CSP (PbCSP) and present CSP-derived peptides to specific H-2k(d) restricted CD8+T-cells with subsequent killing of the presenting cells. We now extend these observations to an in vivo infection model in which infected hepatocytes and antigen specific T-cell clones are transferred into recipient mice inducing protection from sporozoite (SPZ) challenge. In addition, using a similar protocol, we suggest the capacity of hepatocytes in priming of naïve T-cells to provide protection, as further confirmed by induction of protection after depletion of cross-presenting dendritic cells (DCs) by cytochrome c (cyt c) treatment or using traversal deficient parasites. Our results clearly show that hepatocytes present Plasmodium CSP to specific-primed CD8+T-cells, and could also prime naïve T-cells, leading to protection from infection. These results could contribute to a better understanding of liver stage immune response and design of malaria vaccines.

Statistical modelling of CSP solving algorithms performance

The goal of this work is to try to create a statistical model, based only on easily computable parameters from the CSP problem to predict runtime behaviour of the solving algorithms, and let us choose the best algorithm to solve the problem. Although it seems that the obvious choice should be MAC, experimental results obtained so far show, that with big numbers of variables, other algorithms perfom much better, specially for hard problems in the transition phase.

Generating hard SAT/CSP instances using expander graphs

In this paper we provide a new method to generate hard k-SAT instances. We incrementally construct a high girth bipartite incidence graph of the k-SAT instance. Having high girth assures high expansion for the graph, and high expansion implies high resolution width. We have extended this approach to generate hard n-ary CSP instances and we have also adapted this idea to increase the expansion of the system of linear equations used to generate XORSAT instances, being able to produce harder satisfiable instances than former generators.

Edge matching puzzles as hard SAT/CSP benchmarks

Recently, edge matching puzzles, an NP-complete problem, have rececived, thanks to money-prized contests, considerable attention from wide audiences. We consider these competitions not only a challenge for SAT/CSP solving techniques but also as an opportunity to showcase the advances in the SAT/CSP community to a general audience. This paper studies the NP-complete problem of edge matching puzzles focusing on providing generation models of problem instances of variable hardness and on its resolution through the application of SAT and CSP techniques. From the generation side, we also identify the phase transition phenomena for each model. As solving methods, we employ both; SAT solvers through the translation to a SAT formula, and two ad-hoc CSP solvers we have developed, with different levels of consistency, employing several generic and specialized heuristics. Finally, we conducted an extensive experimental investigation to identify the hardest generation models and the best performing solving techniques.