Formal Specification of Relational Model of Data in Z-Notation

Владимир Димитров - Целта на настоящия доклад е формалната спецификация на релационния модел на данни. Тази спецификация след това може да бъде разширена към Обектно-релационния модел на данни и към Потоците от данни.

modern foreign languages classroom:is inclusion of all exclusion in disguise?

The past decade has seen a drive to give all pupils the opportunity to study a Modern Foreign Language (MFL) in schools in England, making the teaching and learning of foreign languages part of the primary school curriculum. The Languages for All: Languages for Life (DfES, 2002) policy was introduced through the National Languages Strategy with an objective to increase the nation’s language capability. Raising the educational standard for all pupils is another government initiative with a strong emphasis on inclusion. As the Languages for All policy stresses the importance and benefits of language learning, and inclusion suggests equality and provision for all, this study examines the inclusion of all key stage 2 pupils in foreign language learning and describes perceptions and experiences of pupils, particularly those identified as having special educational needs (SEN) in their performances and negotiations in learning French. As a small scale, qualitative and ethnographically informed, this research is based on participant observation and semi-structured interviews with pupils, teachers of French, teaching assistants and parents. This study draws upon Nussbaum’s capabilities approach and Bourdieu’s concepts as theoretical foundations to analyse the ‘inclusive’ French classroom. As the capabilities approach takes people as ends not means, and goes beyond a focus on resources, it lends itself to critical thinking on issues around inclusion in education. In this context, this researcher investigates the experiences of pupils who struggle with foreign language learning because of their abilities or disabilities, and frames the discussion around the capabilities approach. The study also focuses on motivation and identity in foreign language learning, and draws upon Bourdieu’s concepts of capital, habitus and field to analyse how the participants make sense of and respond to their own circumstances in relation to their performances in the language learning process. This research thus considers Bourdieu’s concepts for a deeper understanding of issues of inequality in learning French and takes up Nussbaum’s insight that pupils may differ in what learning French means to them, and it is not how they differ, but the difference between their capability to choose and achieve what they value that should matter. The findings indicate that although, initially, the French classroom appears ‘inclusive’ due to the provision and practices of inclusion, a closer look shows it to be exclusionary. In addition, responses from the participants on the usefulness and benefits of foreign language learning are contradictory to the objectives of the Languages for All policy, illustrating the complexity of the ‘inclusive’ MFL classroom. This research concludes that structural and interpersonal practices of inclusion contribute to the disguising of exclusion in a classroom deemed ‘inclusive’. Implications are that an understanding and consideration of other aspect of life such as well-being, interests, needs and values should form a necessary part of the language policy.

Specification and quantitative analysis of probabilistic cloud deployment patterns

Cloud computing is a new technological paradigm offering computing infrastructure, software and platforms as a pay-as-you-go, subscription-based service. Many potential customers of cloud services require essential cost assessments to be undertaken before transitioning to the cloud. Current assessment techniques are imprecise as they rely on simplified specifications of resource requirements that fail to account for probabilistic variations in usage. In this paper, we address these problems and propose a new probabilistic pattern modelling (PPM) approach to cloud costing and resource usage verification. Our approach is based on a concise expression of probabilistic resource usage patterns translated to Markov decision processes (MDPs). Key costing and usage queries are identified and expressed in a probabilistic variant of temporal logic and calculated to a high degree of precision using quantitative verification techniques. The PPM cost assessment approach has been implemented as a Java library and validated with a case study and scalability experiments. © 2012 Springer-Verlag Berlin Heidelberg.

Something to talk about: Content and Language Integrated Learning in Modern Languages in British Higher Education. A case study of German at Aston University

This thesis investigates Content and Language Integrated Learning (CLIL) in German undergraduate programmes in the UK. At its core is a study of how one German department integrates the teaching of language and content in its undergraduate programmes and how instructors and students experience this approach. This micro-context is embedded in the wider macro-context of UK Higher Education and subject to outside forces - be they political, economic, socio-cultural - whose effects will manifest in more or less obvious ways. Data was collected via an online survey of Heads of German at British universities to determine the status quo of CLIL in UK Higher Education and to investigate how certain institutional parameters determine the introduction of CLIL in Higher Education. This project employs a mixed-method case study approach and is based on student questionnaires and semi-structured interview with German teaching staff. The study brings to light a number of significant aspects. For example, contrary to popular belief, content provision in the L2 is rather common at British universities, which is currently not reflected in the research. Student data indicates that German students perceive clear advantages in the university’s approach to CLIL. They consider German-taught content classes challenging yet beneficial for their language development. Staff interviews have yielded intriguing information about perceived advantages and disadvantages of CLIL, about its implications for classroom practice, and about instructors’ attitude towards teacher training, which echo findings from similar investigations in European contexts. Finally, the results of the macro-analysis and the case study are compared and contrasted with findings from European research on ICLHE/CLIL to determine differences and similarities with the British context, a set of recommendations is made regarding CLIL practice at the case study institution, and some implications these indings may have for the future of CLIL in British higher education are discussed.

Web-based report generators, data visualization, and Web-to-database connectivity

Because some Web users will be able to design a template to visualize information from scratch, while other users need to automatically visualize information by changing some parameters, providing different levels of customization of the information is a desirable goal. Our system allows the automatic generation of visualizations given the semantics of the data, and the static or pre-specified visualization by creating an interface language. We address information visualization taking into consideration the Web, where the presentation of the retrieved information is a challenge. ^ We provide a model to narrow the gap between the user's way of expressing queries and database manipulation languages (SQL) without changing the system itself thus improving the query specification process. We develop a Web interface model that is integrated with the HTML language to create a powerful language that facilitates the construction of Web-based database reports. ^ As opposed to other papers, this model offers a new way of exploring databases focusing on providing Web connectivity to databases with minimal or no result buffering, formatting, or extra programming. We describe how to easily connect the database to the Web. In addition, we offer an enhanced way on viewing and exploring the contents of a database, allowing users to customize their views depending on the contents and the structure of the data. Current database front-ends typically attempt to display the database objects in a flat view making it difficult for users to grasp the contents and the structure of their result. Our model narrows the gap between databases and the Web. ^ The overall objective of this research is to construct a model that accesses different databases easily across the net and generates SQL, forms, and reports across all platforms without requiring the developer to code a complex application. This increases the speed of development. In addition, using only the Web browsers, the end-user can retrieve data from databases remotely to make necessary modifications and manipulations of data using the Web formatted forms and reports, independent of the platform, without having to open different applications, or learn to use anything but their Web browser. We introduce a strategic method to generate and construct SQL queries, enabling inexperienced users that are not well exposed to the SQL world to build syntactically and semantically a valid SQL query and to understand the retrieved data. The generated SQL query will be validated against the database schema to ensure harmless and efficient SQL execution. (Abstract shortened by UMI.)^

What secondary English to speakers of other languages (ESOL) teachers know about social and academic language and instructional strategies for limited English proficient students

The purpose of this study was to examine what secondary English to Speakers of Other Languages (ESOL) teachers understand about social and academic language, what instructional strategies they use for Limited English Proficient (LEP) students, and how these concepts are operationalized in their daily practice. ^ This was a mixed method study incorporating both quantitative and qualitative data collection and interpretation. Written questionnaires and individual interviews addressed the questions on teachers' definitions of social and academic language and their strategy use. Classroom observations provided verification of their definitions and their descriptions of instruction for academic language. ^ Findings indicated that teachers' definitions of social and academic language were still developing and that there were ambiguities in identifying examples of social and academic language. The use of graphic organizers or visual supports, groups or peer partners, role play or drama, and modeling were the strategies teachers consistently listed for beginner, intermediate, advanced and multiple level classes. Additionally, teachers' descriptions of their instruction were congruent with what was observed in their classroom practice. ^ It appeared that this population of secondary ESOL teachers was in the process of evolving their definitions of social and academic language and were at different stages in this evolution. Teachers' definitions of language influenced their instruction. Furthermore, those who had clear constructs of language were able to operationalize them in their classroom instruction. ^

Refinement methods for software architecture design using the software architecture model

Modern software systems are often large and complicated. To better understand, develop, and manage large software systems, researchers have studied software architectures that provide the top level overall structural design of software systems for the last decade. One major research focus on software architectures is formal architecture description languages, but most existing research focuses primarily on the descriptive capability and puts less emphasis on software architecture design methods and formal analysis techniques, which are necessary to develop correct software architecture design. ^ Refinement is a general approach of adding details to a software design. A formal refinement method can further ensure certain design properties. This dissertation proposes refinement methods, including a set of formal refinement patterns and complementary verification techniques, for software architecture design using Software Architecture Model (SAM), which was developed at Florida International University. First, a general guideline for software architecture design in SAM is proposed. Second, specification construction through property-preserving refinement patterns is discussed. The refinement patterns are categorized into connector refinement, component refinement and high-level Petri nets refinement. These three levels of refinement patterns are applicable to overall system interaction, architectural components, and underlying formal language, respectively. Third, verification after modeling as a complementary technique to specification refinement is discussed. Two formal verification tools, the Stanford Temporal Prover (STeP) and the Simple Promela Interpreter (SPIN), are adopted into SAM to develop the initial models. Fourth, formalization and refinement of security issues are studied. A method for security enforcement in SAM is proposed. The Role-Based Access Control model is formalized using predicate transition nets and Z notation. The patterns of enforcing access control and auditing are proposed. Finally, modeling and refining a life insurance system is used to demonstrate how to apply the refinement patterns for software architecture design using SAM and how to integrate the access control model. ^ The results of this dissertation demonstrate that a refinement method is an effective way to develop a high assurance system. The method developed in this dissertation extends existing work on modeling software architectures using SAM and makes SAM a more usable and valuable formal tool for software architecture design. ^

Security specification and enforcement in mediation system

Mediation techniques provide interoperability and support integrated query processing among heterogeneous databases. While such techniques help data sharing among different sources, they increase the risk for data security, such as violating access control rules. Successful protection of information by an effective access control mechanism is a basic requirement for interoperation among heterogeneous data sources. ^ This dissertation first identified the challenges in the mediation system in order to achieve both interoperability and security in the interconnected and collaborative computing environment, which includes: (1) context-awareness, (2) semantic heterogeneity, and (3) multiple security policy specification. Currently few existing approaches address all three security challenges in mediation system. This dissertation provides a modeling and architectural solution to the problem of mediation security that addresses the aforementioned security challenges. A context-aware flexible authorization framework was developed in the dissertation to deal with security challenges faced by mediation system. The authorization framework consists of two major tasks, specifying security policies and enforcing security policies. Firstly, the security policy specification provides a generic and extensible method to model the security policies with respect to the challenges posed by the mediation system. The security policies in this study are specified by 5-tuples followed by a series of authorization constraints, which are identified based on the relationship of the different security components in the mediation system. Two essential features of mediation systems, i. e., relationship among authorization components and interoperability among heterogeneous data sources, are the focus of this investigation. Secondly, this dissertation supports effective access control on mediation systems while providing uniform access for heterogeneous data sources. The dynamic security constraints are handled in the authorization phase instead of the authentication phase, thus the maintenance cost of security specification can be reduced compared with related solutions. ^

Practical secure information flow in programming languages

If we classify variables in a program into various security levels, then a secure information flow analysis aims to verify statically that information in a program can flow only in ways consistent with the specified security levels. One well-studied approach is to formulate the rules of the secure information flow analysis as a type system. A major trend of recent research focuses on how to accommodate various sophisticated modern language features. However, this approach often leads to overly complicated and restrictive type systems, making them unfit for practical use. Also, problems essential to practical use, such as type inference and error reporting, have received little attention. This dissertation identified and solved major theoretical and practical hurdles to the application of secure information flow. ^ We adopted a minimalist approach to designing our language to ensure a simple lenient type system. We started out with a small simple imperative language and only added features that we deemed most important for practical use. One language feature we addressed is arrays. Due to the various leaking channels associated with array operations, arrays have received complicated and restrictive typing rules in other secure languages. We presented a novel approach for lenient array operations, which lead to simple and lenient typing of arrays. ^ Type inference is necessary because usually a user is only concerned with the security types for input/output variables of a program and would like to have all types for auxiliary variables inferred automatically. We presented a type inference algorithm B and proved its soundness and completeness. Moreover, algorithm B stays close to the program and the type system and therefore facilitates informative error reporting that is generated in a cascading fashion. Algorithm B and error reporting have been implemented and tested. ^ Lastly, we presented a novel framework for developing applications that ensure user information privacy. In this framework, core computations are defined as code modules that involve input/output data from multiple parties. Incrementally, secure flow policies are refined based on feedback from the type checking/inference. Core computations only interact with code modules from involved parties through well-defined interfaces. All code modules are digitally signed to ensure their authenticity and integrity. ^

A framework for specification and analysis of software architectures

Software architecture is the abstract design of a software system. It plays a key role as a bridge between requirements and implementation, and is a blueprint for development. The architecture represents a set of early design decisions that are crucial to a system. Mistakes in those decisions are very costly if they remain undetected until the system is implemented and deployed. This is where formal specification and analysis fits in. Formal specification makes sure that an architecture design is represented in a rigorous and unambiguous way. Furthermore, a formally specified model allows the use of different analysis techniques for verifying the correctness of those crucial design decisions. ^ This dissertation presented a framework, called SAM, for formal specification and analysis of software architectures. In terms of specification, formalisms and mechanisms were identified and chosen to specify software architecture based on different analysis needs. Formalisms for specifying properties were also explored, especially in the case of non-functional properties. In terms of analysis, the dissertation explored both the verification of functional properties and the evaluation of non-functional properties of software architecture. For the verification of functional property, methodologies were presented on how to apply existing model checking techniques on a SAM model. For the evaluation of non-functional properties, the dissertation first showed how to incorporate stochastic information into a SAM model, and then explained how to translate the model to existing tools and conducts the analysis using those tools. ^ To alleviate the analysis work, we also provided a tool to automatically translate a SAM model for model checking. All the techniques and methods described in the dissertation were illustrated by examples or case studies, which also served a purpose of advocating the use of formal methods in practice. ^

An integrated framework for ensuring the quality of software design

Software development is an extremely complex process, during which human errors are introduced and result in faulty software systems. It is highly desirable and important that these errors can be prevented and detected as early as possible. Software architecture design is a high-level system description, which embodies many system features and properties that are eventually implemented in the final operational system. Therefore, methods for modeling and analyzing software architecture descriptions can help prevent and reveal human errors and thus improve software quality. Furthermore, if an analyzed software architecture description can be used to derive a partial software implementation, especially when the derivation can be automated, significant benefits can be gained with regard to both the system quality and productivity. This dissertation proposes a framework for an integrated analysis on both of the design and implementation. To ensure the desirable properties of the architecture model, we apply formal verification by using the model checking technique. To ensure the desirable properties of the implementation, we develop a methodology and the associated tool to translate an architecture specification into an implementation written in the combination of Arch-Java/Java/AspectJ programming languages. The translation is semi-automatic so that many manual programming errors can be prevented. Furthermore, the translation inserting monitoring code into the implementation such that runtime verification can be performed, this provides additional assurance for the quality of the implementation. Moreover, validations for the translations from architecture model to program are provided. Finally, several case studies are experimented and presented.

Enabling adaptability in service aggregates using transparent shaping techniques

Distributed applications are exposed as reusable components that are dynamically discovered and integrated to create new applications. These new applications, in the form of aggregate services, are vulnerable to failure due to the autonomous and distributed nature of their integrated components. This vulnerability creates the need for adaptability in aggregate services. The need for adaptation is accentuated for complex long-running applications as is found in scientific Grid computing, where distributed computing nodes may participate to solve computation and data-intensive problems. Such applications integrate services for coordinated problem solving in areas such as Bioinformatics. For such applications, when a constituent service fails, the application fails, even though there are other nodes that can substitute for the failed service. This concern is not addressed in the specification of high-level composition languages such as that of the Business Process Execution Language (BPEL). We propose an approach to transparently autonomizing existing BPEL processes in order to make them modifiable at runtime and more resilient to the failures in their execution environment. By transparent introduction of adaptive behavior, adaptation preserves the original business logic of the aggregate service and does not tangle the code for adaptive behavior with that of the aggregate service. The major contributions of this dissertation are: first, we assessed the effectiveness of BPEL language support in developing adaptive mechanisms. As a result, we identified the strengths and limitations of BPEL and came up with strategies to address those limitations. Second, we developed a technique to enhance existing BPEL processes transparently in order to support dynamic adaptation. We proposed a framework which uses transparent shaping and generative programming to make BPEL processes adaptive. Third, we developed a technique to dynamically discover and bind to substitute services. Our technique was evaluated and the result showed that dynamic utilization of components improves the flexibility of adaptive BPEL processes. Fourth, we developed an extensible policy-based technique to specify how to handle exceptional behavior. We developed a generic component that introduces adaptive behavior for multiple BPEL processes. Fifth, we identify ways to apply our work to facilitate adaptability in composite Grid services.

Formal modeling and analysis techniques for high level Petri nets

Petri Nets are a formal, graphical and executable modeling technique for the specification and analysis of concurrent and distributed systems and have been widely applied in computer science and many other engineering disciplines. Low level Petri nets are simple and useful for modeling control flows but not powerful enough to define data and system functionality. High level Petri nets (HLPNs) have been developed to support data and functionality definitions, such as using complex structured data as tokens and algebraic expressions as transition formulas. Compared to low level Petri nets, HLPNs result in compact system models that are easier to be understood. Therefore, HLPNs are more useful in modeling complex systems. ^ There are two issues in using HLPNs—modeling and analysis. Modeling concerns the abstracting and representing the systems under consideration using HLPNs, and analysis deals with effective ways study the behaviors and properties of the resulting HLPN models. In this dissertation, several modeling and analysis techniques for HLPNs are studied, which are integrated into a framework that is supported by a tool. ^ For modeling, this framework integrates two formal languages: a type of HLPNs called Predicate Transition Net (PrT Net) is used to model a system's behavior and a first-order linear time temporal logic (FOLTL) to specify the system's properties. The main contribution of this dissertation with regard to modeling is to develop a software tool to support the formal modeling capabilities in this framework. ^ For analysis, this framework combines three complementary techniques, simulation, explicit state model checking and bounded model checking (BMC). Simulation is a straightforward and speedy method, but only covers some execution paths in a HLPN model. Explicit state model checking covers all the execution paths but suffers from the state explosion problem. BMC is a tradeoff as it provides a certain level of coverage while more efficient than explicit state model checking. The main contribution of this dissertation with regard to analysis is adapting BMC to analyze HLPN models and integrating the three complementary analysis techniques in a software tool to support the formal analysis capabilities in this framework. ^ The SAMTools developed for this framework in this dissertation integrates three tools: PIPE+ for HLPNs behavioral modeling and simulation, SAMAT for hierarchical structural modeling and property specification, and PIPE+Verifier for behavioral verification.^

The theory of moral sentiments; or, an essay towards an analysis of the principles by wich men naturally judge concerning the conduct and character, first of their neighbours, and afterwards of themselves : to which is added a dissertation on the origin of languages

by Adam Smith, LL.D., fellow of the royal societies of London and Edinburgh, one of the commissioners of his majesty's customs in Scotland, and formerly professor of moral philosophy in the University of Glasgow