1,536 research outputs found
Developing a Consensus Algorithm using Stepwise Refinement
No full textConsensus problems arise in any area of computing where distributedprocesses must come to a joint decision. Although solutions toconsensus problems have similar aims, they vary according to theprocessor faults and network properties that must be taken into account, and modifying theseassumptions will lead to different algorithms. Reasoning about consensusprotocols is subtle, and correctness proofs are often informal.This paper gives a fully formal development and proof of a knownconsensus algorithm using the stepwise refinement method Event-B.This allows us to manage the complexity of the proof process byfactoring the proof of correctness into a number of refinement steps,and to carry out the proof task concurrently with the development.During the development the processor faults and network properties on whichthe development steps rely are identified. The research outlined hereis motivated by the observation that making different choices at thesepoints may lead to alternative algorithms and proofs, leading to arefinement tree of algorithms with partially shared proofs
Formal analysis of access control policies
No full textNVe present a formal (niodel-based) approach to describin, and analvsiiiy access control policies. This approach allows us to evaluate access requests against policies, compare versions of policies with each other and check policies for internal consistency. Access control policies are described tising VDIM, a statebased formal modelling language. Policy descriptions are concise and may be easily manipulated. The structure of the VDIM description is derived from the OASIS standard access control policy language XACML. It is therefore straightforward to translate between XACML policies and their corresponding models
Vascular endothelial growth factor restores delayed tumor progression in tumors depleted of macrophages
No full textGenetic depletion of macrophages in Polyoma Middle T oncoprotein (PyMT)-induced mammary tumors in mice delayed the angiogenic switch and the progression to malignancy. To determine whether vascular endothelial growth factor A (VEGF-A) produced by tumor-associated macrophages regulated the onset of the angiogenic switch, a genetic approach was used to restore expression of VEGF-A into tumors at the benign stages. This stimulated formation of a high-density vessel network and in macrophage-depleted mice, was followed by accelerated tumor progression. The expression of VEGF-A led to a massive infiltration into the tumor of leukocytes that were mostly macrophages. This study suggests that macrophage-produced VEGF regulates malignant progression through stimulating tumor angiogenesis, leukocytic infiltration and tumor cell invasion
Fidelidad del cliente del Hotel JW Marriott el Convento Cusco -2020
No full textEl presente trabajo de investigación se titula “La fidelidad del cliente del hotel JW Marriott El
Convento Cusco-2020”. Teniendo en cuenta que la fidelidad del cliente es un tema que en la
hotelería es uno de los principales intereses y lo vienen desarrollando la mayoría de las cadenas
hoteleras más renombradas, como es Marriott Hotels y específicamente el hotel JW Marriott El
Convento Cusco. En el cual encontramos un problema del cual tratamos en la presente
investigación, la cual se basa en que: si el cliente no pasa satisfactoriamente las fases de
fidelización, no llega a fidelizarse completamente, ello se debe a que existen ciertos aspectos que
impiden una fidelización, es decir que pueden resquebrajar la fidelidad del cliente, por ejemplo los
inconvenientes que puede tener el cliente, ya sea previo al servicio (desde la reserva del servicio
por medio de Online Travel Agency o por otro medio), la entrega o disfrute del servicio (la estadía)
y el post servicio (después del check out del hotel). Por ello, la presente investigación tiene como
objetivo principal describir la fidelidad del cliente del hotel JW Marriott El Convento Cusco-2020.
Como también, los objetivos específicos que describen la fidelidad del cliente en cada una de las
fases de fidelización. La metodología manejada para la elaboración de la presente tesis fue de tipo
cuantitativo, el nivel es descriptivo no experimental.
Se obtuvo datos del autor (Oliver R. , 1999) sobre las fases de la fidelidad del cliente, que son
fidelidad cognitiva, fidelidad afectiva, fidelidad conativa y fidelidad de acción; las cuales se
utilizaron como dimensiones de la variable, describiendo cada una de ellas. Para describir la
fidelidad del cliente del hotel JW Marriott El Convento Cusco-2020 se realizó encuestas vía web
dada la coyuntura actual, con una muestra no probabilística de 102 personas que fueron los clientes
que voluntariamente respondieron el cuestionario.
Según los resultados obtenidos de las encuestas realizadas, se determinó que la fidelidad del cliente
del hotel JW Marriott El Convento Cusco-2020 es muy buena, al igual que sus cuatro fases de
fidelidad del cliente. Debido a que el hotel cumple con todas las expectativas que tiene el cliente y
al final genera una recompra por parte del cliente hacia el hotel JW Marriott El Convento Cusco,
dado por el cumplimiento de las cuatro fases de fidelización del cliente por lo siguiente: El cliente
es inicialmente fiel en un sentido cognitivo basado en la información y creencia que tiene el cliente,
después de las experiencias satisfactorias se genera un sentimiento de compromiso hacia el hotel
siendo fiel afectivamente, para así por medio de intenciones de comportamientos positivos por parte de asociados del hotel siendo fiel conativa, y finalmente el hotel al cumplir con todas las
expectativas del cliente y superar todos los obstáculos posibles se produce un control de la acción
que viene a ser la fidelidad de acción donde se produce la recompra del servicio del hotel JW
Marriott El Convento Cusco y retener al cliente.
Se pudo concluir que, el hotel JW Marriott El Convento Cusco es muy bueno fidelizando a sus
clientes y puede ser mejor incluso, si se siguen las propuestas planteadas. En la investigación, se
ha logrado describir cómo retener a los clientes y generar un compromiso profundo de recompra
del servicio JW Marriott El Convento Cusco por medio de las fases de fidelización.This research is titled “The costumer loyalty of the JW Marriott El Convento Cusco hotel-2020”.
We know that the loyalty in costumers is one of the most important issues for the hospitality
industry and it is been developed by most of the renowned hotel chains in the World, such as
Marriott Hotels and specifically the JW Marriott El Convento Cusco hotel. We found a problem
wich is based on the fact that: if the costumer doesn´t satisfactorily obtain the four loyalty phases,
the client will not become completely loyal to the hotel. This because there are some aspects that
don´t allow the loyalty, for example the pre service (from the reservation of the service through the
Online Travel agency or other method of reservation), the service (the stay) and the post service
(after the check out of the hotel). The main objective of this research is to describe the customer
loyalty of the JW Marriott El Convento Cusco hotel-2020. As well as, the especific objectives, that
describes the customer loyalty in each of the loyalty phases. The methodology used to prepare this
research was quantitative, and the level is descriptive, not experimental.
The data was obtained from the author (Oliver R. , 1999) that explained about the phases of
customer loyalty, which are Cognitive Loyalty, Afective loyalty, Conative loyalty and Action
loyalty; which were used as dimensions, describing each one of them. In order to describe the
costumer loyalty of the JW Marriott El Convento Cusco hotel-2020, we make the surveys via web
because of the current situation, with a non probability sample of 102 people who were the
costumers who voluntarily answered the questionnaire.
The costumer loyalty of the JW Marriott El Convento Cusco hotel -2020 was determined to be very
good, and also the phases of the customer loyalty as well. All that because the hotel meets all the
expectations that the customer has and in the end generates a repurchase by the customer from the
JW Marriott El Convento Cusco hotel, all that with the four phases of the loyalty of the client, and
we can detail that: The cliente initially gets the cognitive loyalty based in the information and
believes that the client has; after the satisfactory experiences, a feeling of commitment to the hotel
is generated, that is the afective loyalty; and for this reason through the intentions of positive
behaviors of the associates of the hotel, that is the conative loyalty; and finally when the hotel
meets all the expectations of the clients and overcoming all the possible obstacles, there is a control
of the action that comes to be the action loyalty, and the repurchase of the service of the JW Marriott
El Convento Cusco hotel occurs and retain more clients. In conclusion, the hotel JW Marriott El Convento Cusco is very good building customers loyalty
and can be better if the proposals proposed are followed. In the research, it has been possible to
describe how to retain customers and generate a deep commitment to repurchase the service of the
JW Marriott El Convento Cusco hotel through the loyalty phases
Developing a consensus algorithm using stepwise refinement
No full textConsensus problems arise in any area of computing where distributed processes must come to a joint decision. Although solutions to consensus problems have similar aims, they vary according to the processor faults and network properties that must be taken into account, and modifying these assumptions will lead to different algorithms. Reasoning about consensus protocols is subtle, and correctness proofs are often informal. This paper gives a fully formal development and proof of a known consensus algorithm using the stepwise refinement method Event-B. This allows us to manage the complexity of the proof process by factoring the proof of correctness into a number of refinement steps, and to carry out the proof task concurrently with the development. During the development the processor faults and network properties on which the development steps rely are identified. The research outlined here is motivated by the observation that making different choices at these points may lead to alternative algorithms and proofs, leading to a refinement tree of algorithms with partially shared proofs
Proceedings of the 7th OVERTURE workshop
No full textThis report contains the proceedings of the 7th OVERTURE workshop, held in Eindhoven on 2nd November 2009
Formal Analysis of BPMN Models Using Event-B
No full textThe use of business process models has gone far beyond documentation purposes. In the development of business applications, they can play the role of an artifact on which high level properties can be verified and design errors can be revealed in an effort to reduce overhead at later software development and diagnosis stages. This paper demonstrates how formal verification may add value to the specification, design and development of business process models in an industrial setting. The analysis of these models is achieved via an algorithmic translation from the de-facto standard business process modeling language BPMN to Event-B, a widely used formal language supported by the Rodin platform which offers a range of simulation and verification technologies
Refinement-based Techniques in the Analysis of Information Flow Policies for Dynamic Virtual Organisations
No full textDynamic virtual organisations (VOs) can arise in situations in which it is critical that they continue to operate, even in sub-optimal environments. Models of information flow in dynamic VOs are therefore needed in order to permit the rigorous verification of resilience properties before commitments are made to implementation. This paper proposes a refinement-based modelling approach for the design and analysis of VO policy resilience. The approach is demonstrated by using the refinement-based formalism Event-B to model a VO structure, commonly referred to as the Bronze/Silver/Gold structure that frequently arises in multi-agency response to emergencies. Machine-assisted proof is used to compare the validity of alternative information flow policies in Bronze/Silver/Gold when a fault is induced in the VO structure
Proceedings of Formal Aspects of Virtual Organisations 2008
No full textThe abstracts and short papers presented at the Formal Aspects of Virtual Organisations workshop (FAVO 2008), held in conjunction with FM\u2708
- …
