Incremental Development of RBAC-Controlled E-Marking System Using the B Method

2015 ◽  
Author(s):  
Nasser Al-Hadhrami ◽  
Benjamin Aziz ◽  
Shantanu Sardesai ◽  
Lotfi ben Othmane
Keyword(s):  
Incremental Development ◽  
B Method

scholarly journals A Mechanically Proved and an Incremental Development of the Session Initiation Protocol INVITE Transaction

2014 ◽  
Vol 2014 ◽  
pp. 1-11
Author(s):  
Rajaa Filali ◽  
Mohamed Bouhdadi
Keyword(s):  
Session Initiation Protocol ◽  
Application Layer ◽  
Levels Of Abstraction ◽  
Signaling Protocol ◽  
Incremental Development ◽  
B Method ◽  
Almost All ◽  
Event B Method ◽  
Different Levels

The Session Initiation Protocol (SIP) is an application layer signaling protocol used to create, manage, and terminate sessions in an IP based network. SIP is considered as a transactional protocol. There are two main SIP transactions, the INVITE transaction and the non-INVITE transaction. The SIP INVITE transaction specification is described in an informal way in Request for Comments (RFC) 3261 and modified in RFC 6026. In this paper we focus on the INVITE transaction of SIP, over reliable and unreliable transport mediums, which is used to initiate a session. In order to ensure the correctness of SIP, the INVITE transaction is modeled and verified using event-B method and its Rodin platform. The Event-B refinement concept allows an incremental development by defining the studied system at different levels of abstraction, and Rodin discharges almost all proof obligations at each level. This interaction between modeling and proving reduces the complexity and helps in assuring that the INVITE transaction SIP specification is correct, unambiguous, and easy to understand.

Modeling and Re-Evaluating Security in an Incremental Development of RBAC-Based Systems Using B Method

2019 ◽  
pp. 104-135
Author(s):  
Nasser Al-Mur Al-Hadhrami
Keyword(s):  
Access Control ◽  
Software Development ◽  
Role Based Access Control ◽  
Incremental Development ◽  
B Method ◽  
Access Control Models ◽  
Iterative Development ◽  
Role Based

Incremental software development through the addition of new features and access rules potentially creates security flaws due to inconsistent access control models. Discovering such flaws in software architectures is commonly performed with formal techniques that allow the verification of the correctness of a system and its compliance with applicable policies. In this chapter, the authors propose the use of the B method to formally, and incrementally, design and evaluate the security of systems running under role-based access control (RBAC) policies. They use an electronic marking system (EMS) as a case study to demonstrate the iterative development of RBAC models and the role of the B language in exploring and re-evaluating the security of the system as well as addressing inconsistencies caused by incremental software development. Two formal approaches of model checking and proof obligations are used to verify the correctness of the RBAC specification.

scholarly journals Informing patients: The Bolam legacy

2020 ◽  
Vol 20 (2) ◽  
pp. 103-130
Author(s):  
Emma Cave ◽  
Caterina Milo
Keyword(s):  
Hospital Management ◽  
Medical Advice ◽  
Diagnosis And Treatment ◽  
Health Board ◽  
Management Committee ◽  
Patient Centred Care ◽  
Capacity To Consent ◽  
Incremental Development ◽  
The Uk ◽  
Treatment Alternatives

In the context of medical advice to patients, the UK decision in Montgomery v. Lanarkshire Health Board rejected the application of Bolam v. Friern Hospital Management Committee. This article argues that the rejection is neither complete nor settled. We explore doctrinal, conceptual and practical limitations of Montgomery to demonstrate the vestiges of Bolam’s relevance to medical advice. Medical advice does not end with disclosure of material risk but incorporates information on prognosis, diagnosis and treatment alternatives. Montgomery does not always apply in these cases, nor outside the medical mainstream or where patients lack capacity to consent. We identify ways in which the extension of patient-centred care in the giving of medical advice can be achieved through incremental development of Montgomery and application of the Bolitho gloss to require that processes conform to Montgomery principles of partnership and autonomy.

The incremental development process in Cleanroom software engineering

1996 ◽  
Vol 17 (1) ◽  
pp. 55-71 ◽  
Author(s):  
Carmen J. Trammell ◽  
Mark G. Pleszkoch ◽  
Richard C. Linger ◽  
Alan R. Hevner
Keyword(s):  
Software Engineering ◽  
Development Process ◽  
Incremental Development

scholarly journals Supporting the development of scientific understanding when constructing an evolving explanation

2022 ◽  
Vol 4 (1) ◽  
Author(s):  
Ann M. Novak ◽  
David F. Treagust
Keyword(s):  
Scientific Explanation ◽  
Project Based Learning ◽  
Incremental Development ◽  
Freshwater Organisms ◽  
Freshwater System ◽  
New Evidence ◽  
Scientific Ideas ◽  
Over Time

AbstractWe explore how students developed an integrated understanding of scientific ideas and how they applied their understandings in new situations. We examine the incremental development of 7th grade students’ scientific ideas across four iterations of a scientific explanation related to a freshwater system. We demonstrate that knowing how to make use of scientific ideas to explain phenomena needs to be learned just as developing integrated understanding of scientific ideas needs to be learned. Students participated in an open-ended, long-term project-based learning unit, constructing one explanation over time to address, “How healthy is our stream for freshwater organisms and how do our actions on land potentially impact the water quality of the stream?” The explanation developed over several weeks as new data were collected and analyzed. Students discussed evidence by revisiting scientific ideas and including new scientific ideas. This research investigates two questions: (1) As students engage in writing a scientific explanation over time, to what extent do they develop integrated understanding of appropriate scientific ideas? and (2) When writing about new evidence, do these earlier experiences of writing explanations enable students to make use of new scientific ideas in more sophisticated ways? In other words, do earlier experiences allow students to know how to make use of their ideas in these new situations? The results indicated statistically significant effects. Through various iterations of the explanation students included richer discussion using appropriate scientific ideas. Students were also able to make better use of new knowledge in new situations.

scholarly journals Validation of Component based Software Development Model using Formal B-Method

2013 ◽  
Vol 67 (9) ◽  
pp. 24-35 ◽  
Author(s):  
Asif IrshadKhan ◽  
Md. Mottahir Alam ◽  
Noor-ul-Qayyum Noor-ul-Qayyum ◽  
Usman Ali Khan
Keyword(s):  
Software Development ◽  
Development Model ◽  
B Method ◽  
Software Development Model
Sign in / Sign up

Export Citation Format

Share Document