排序方式: 共有11条查询结果,搜索用时 15 毫秒
1.
2.
eb
3 is a trace-based formal language created for the specification of information systems. In eb
3, each entity and association attribute is independently defined by a recursive function on the valid traces of external events.
This paper describes an algorithm that generates, for each external event, a transaction that updates the value of affected
attributes in their relational database representation. The benefits are twofold: eb
3 attribute specifications are automatically translated into executable programs, eliminating system design and implementation
steps; the construction of information systems is streamlined, because eb
3 specifications are simpler and shorter to write than corresponding traditional specifications, design and implementations.
In particular, the paper shows that simple eb
3 constructs can replace complex SQL queries which are typically difficult to write.
相似文献
Régine LaleauEmail: |
3.
4.
J. Milhau A. Idani R. Laleau M. A. Labiadh Y. Ledru M. Frappier 《Innovations in Systems and Software Engineering》2011,7(4):303-313
Combination of formal and semi-formal methods is more and more required to produce specifications that can be, on the one
hand, understood and thus validated by both designers and users and, on the other hand, precise enough to be verified by formal
methods. This motivates our aim to use these complementary paradigms in order to deal with security aspects of information
systems. This paper presents a methodology to specify access control policies starting with a set of graphical diagrams: UML
for the functional model, SecureUML for static access control and ASTD for dynamic access control. These diagrams are then
translated into a set of B machines. Finally, we present the formal specification of an access control filter that coordinates
the different kinds of access control rules and the specification of functional operations. The goal of such B specifications
is to rigorously check the access control policy of an information system taking advantage of tools from the B method. 相似文献
5.
Extending statecharts with process algebra operators 总被引:3,自引:2,他引:1
Marc Frappier Frédéric Gervais Régine Laleau Benoît Fraikin Richard St-Denis 《Innovations in Systems and Software Engineering》2008,4(3):285-292
This paper describes an adaptation of statecharts to take advantage of process algebra operators like those found in CSP and
EB3. The resulting notation is called algebraic state transition diagrams (ASTDs). The process algebra operators considered include sequence, iteration, parallel composition, and quantified synchronization.
Quantification is one of the salient features of ASTDs, because it provides a powerful mechanism to precisely and explicitly
define cardinalities in a dynamic model. The formal semantics of ASTDs is expressed using the operational style typically
used in process algebras. The target application domain is the specification and implementation of information systems. 相似文献
6.
This paper compares two formal methods, B and eb3, for specifying information systems. These two methods are chosen as examples of the state-based paradigm and the event-based paradigm, respectively. The paper considers four viewpoints: functional behavior expression, validation, verification, and evolution. Issues in expressing event ordering constraints, data integrity constraints, and modularity are thereby considered. A simple case study is used to illustrate the comparison, namely, a library management system. Two equivalent specifications are presented using each method. The paper concludes that B and eb3 are complementary. The former is better at expressing complex ordering and static data integrity constraints, whereas the latter provides a simpler, modular, explicit representation of dynamic constraints that are closer to the user’s point of view, while providing loosely coupled definitions of data attributes. The generality of these results from the state-based paradigm and the event-based paradigm perspective are discussed. 相似文献
7.
Régine Laleau Farida Semmak Abderrahman Matoussi Dorian Petit Ahmed Hammad Bruno Tatibouet 《Innovations in Systems and Software Engineering》2010,6(1-2):47-54
This article describes a work-in-progress in the framework of a research project aiming at combining requirements engineering methods with formal methods. The main idea is to extend the SysML language with concepts of existing requirements engineering methods. In this article we present extensions to SysML with concepts from the goal model of the KAOS method and we give rules to derive a formal B specification from this goal model. The approach is then illustrated on a case study. 相似文献
8.
Using formal metamodels to check consistency of functional views in information systems specification 总被引:1,自引:0,他引:1
UML notations require adaptation for applications such as Information Systems (IS). Thus we have defined IS-UML. The purpose of this article is twofold. First, we propose an extension to this language to deal with functional aspects of IS. We use two views to specify IS transactions: the first one is defined as a combination of behavioural UML diagrams (collaboration and state diagrams), and the second one is based on the definition of specific classes of an extended class diagram. The final objective of the article is to consider consistency issues between the various diagrams of an IS-UML specification. In common with other UML languages, we use a metamodel to define IS-UML. We use class diagrams to summarize the metamodel structure and a formal language, B, for the full metamodel. This allows us to formally express consistency checks and mapping rules between specific metamodel concepts. 相似文献
9.
A formal approach based on UML and B for the specification and development of database applications 总被引:1,自引:0,他引:1
This article describes a formal approach to specify and develop database applications. This approach consists of two complementary
phases. In the first phase, B specifications are automatically generated from UML class, state and collaboration diagrams
describing the data and the transactions of the system we are developing. In the second phase, these specifications are successively
refined until they become close enough to a relational implementation. The tool supporting this approach is implemented as
an extension of the Rational Rose tool to develop and visualize graphical (UML) and formal (B) notations in a single environment. 相似文献
10.
Marc Frappier Frédéric Gervais Régine Laleau Jérémy Milhau 《Formal Aspects of Computing》2014,26(5):919-941
This paper introduces three refinement patterns for algebraic state-transition diagrams (astds): state refinement, transition refinement and loop-transition refinement. These refinement patterns are derived from practice in using astds for specifying information systems and security policies in two industrial research projects. Two refinement relations used in these patterns are formally defined. For each pattern, proof obligations are proposed to ensure preservation of behaviour through refinement. The proposed refinement relations essentially consist in preserving scenarios by replacing abstract events with concrete events, or by introducing new events. Deadlocks cannot be introduced; divergence over new events is allowed in one of the refinement relation. We prove congruence-like properties for these three patterns, in order to show that they can be applied to a subpart of a specification while preserving global properties. These three refinement patterns are illustrated with a simple case study of a complaint management system. 相似文献