An MDA approach towards integrating formal and informal modeling languages

This paper shows how formal and informal modeling languages can be cooperatively used in the MDA framework, and how transformations between models in these languages can be achieved using an MDA development environment. The integrated approach also provides an effective V&V technique for the MDA.

Implementation of a triple modular redundant FPGA based safety critical system for reliable software execution

This paper describes the implementation of a TMR (Triple Modular Redundant) microprocessor system on a FPGA. The system exhibits true redundancy in that three instances of the same processor system (both software and hardware) are executed in parallel. The described system uses software to control external peripherals and a voter is used to output correct results. An error indication is asserted whenever two of the three outputs match or all three outputs disagree. The software has been implemented to conform to a particular safety critical coding guideline/standard which is popular in industry. The system was verified by injecting various faults into it.

A technique for modular logic program refinement

A refinement calculus provides a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. In this paper we introduce modules into a logic programming refinement calculus. Modules allow data types to be grouped together with sets of procedures that manipulate the data types. By placing restrictions on the way a program uses a module, we develop a technique for refining the module so that it uses a more efficient representation of the data type.

Linking Agentive Objects in Mandarin Chinese

This paper is concerned with the problem of argument-function mismatch observed in the apparent subject-object inversion in Chinese consumption verbs, e.g., chi 'eat' and he 'drink', and accommodation verbs, e.g., zhu 'live' and shui 'sleep'. These verbs seem to allow the linking of [agent-SUBJ theme-OBJ] as well as [agent-OBJ theme-SUBJ], but only when the agent is also the semantic role denoting the measure or extent of the action. The account offered is formulated within LFG's lexical mapping theory. Under the simplest and also the strictest interpretation of the one-to-one argument-function mapping principle (or the theta-criterion), a composite role such as ag-ext receives syntactic assignment via one composing role only. One-to-one linking thus entails the suppression of the other composing role. Apparent subject-object inversion occurs when the more prominent agent role is suppressed and thus allows the less prominent extent role to dictate the linking of the entire ag-ext composite role. This LMT account also potentially facilitates a natural explanation of markedness among the competing syntactic structures.

Prosody of tone Sandhi in Vietnamese reduplications

In this paper we take advantage of the segmental control afforded by full and partial Vietnamese reduplication on a constant carrier phrase to obtain acoustic evidence of assymetrical prominence relations (van der Hulst 2005), in support of a hypothesis that Vietnamese reduplications are phonetically right headed and that tone sandhi is a reduction phenomenon occurring on prosodically weak positions (Shih 2005). Acoustic parameters of syllable duration (onset, nucleus and coda), F0 range, F0 contour, vowel intensity, spectral tilt and vowel formant structure are analyzed to determine: (1) which syllable of the two (base or reduplicant) is more prominent and (2) how the tone sandhi forms differ from their full reduplicated counterparts. Comparison of full and partial reduplicant syllables in tone sandhi forms provide additional support for this analysis.

Modal functions of future tenses in French

The paper disputes two influential claims in the Romance Linguistics literature. The first is that the synthetic future tenses in spoken Western Romance are now rivalled, if not supplanted, as temporal functors by the more recently developed GO futures. The second is that these synthetic futures now have modal rather than temporal meanings in spoken Romance. These claims are seen as reflecting a universal cycle of diachronic change, in which verb forms originally expressing modal (or aspectual) values take on future temporal reference, becoming tenses. The new modal meanings supplant the temporal, which are then taken up by new forms. Challenges to this theory for French are raised on the basis of empirical evidence of two sorts. Positively, future tenses in spoken Romance continue to be used with temporal meaning. Negatively, evidence of modal meaning for these forms is lacking. The evidence comes froma corpora of spoken French, native speaker judgements and verb data from a daily broadsheet. Cumulatively, it points to the reverse of the claims noted above: the synthetic future in spoken French has temporal but little modal meaning.

Norwegian long-distance reflexives: Lectal variation and speaker attitudes

10 lectal variables were examined with respect to Norwegian speakers' acceptance of long-distance reflexives (LDR), using a questionnaire to elicit grammaticality judgements on 50 potential LDR sentences. A sample of 180 speakers completed the questionnaire. The data was analysed using a general linear model univariate model, and Spearman's correlation. In this sample the results showed that dialect and level of education had significant effects on speakers' acceptance of long-distance reflexives, while sex, age, being a native speaker, having both native-speaker parents, living in the city or the country, and the speaker's attitudes to the two Norwegian writing languages had no influence on speakers' acceptance of long-distance reflexives. It is suggested that the influence of Danish on Norwegian writing and on the southern dialects may be the cause of the observed variation with respect to LDR in Norwegian.

The predicate marker li in Mauritian Creole

There is a morpheme 'li' in Mauritian Creole (MC), which is homophonous with the 3sg pronoun, and which, in the early creole, occurs frequently between the subject and the predicate in affirmative, present tense clauses. I propose that that 'li' may have originated as a resumptive pronoun, co-referential with the subject, but following the grammaticalization of new determiner elements to mark the semantic contrasts of [±definite] and singular vs. plural, 'li' has now grammaticalized into a predicate marker. Its presence is sensitive to both the nature of the predicate, and to the definiteness and specificity features of the subject NP. My analysis is within the framework of Truth Conditional Semantics, where indefinite NPs are analyzed as variables that get introduced into the discourse, and must be bound by an operator to yield a closed proposition, with a truth value. Drawing on a comparison with a cognative morpheme 'i' in Seychellois Creole, I claim that its path to grammaticalization is linked to that of the specificity marking 'la'.

A Fibred Tableau Calculus for Modal Logics of Agents

In previous works we showed how to combine propositional multimodal logics using Gabbay's \emph{fibring} methodology. In this paper we extend the above mentioned works by providing a tableau-based proof technique for the combined/fibred logics. To achieve this end we first make a comparison between two types of tableau proof systems, (\emph{graph} $\&$ \emph{path}), with the help of a scenario (The Friend's Puzzle). Having done that we show how to uniformly construct a tableau calculus for the combined logic using Governatori's labelled tableau system \KEM. We conclude with a discussion on \KEM's features.